waybel13.miz



    begin

    theorem :: WAYBEL13:1

    

     Th1: for L be non empty reflexive transitive RelStr holds for x,y be Element of L holds x <= y implies ( compactbelow x) c= ( compactbelow y)

    proof

      let L be non empty reflexive transitive RelStr;

      let x,y be Element of L;

      assume

       A1: x <= y;

      now

        let z be object;

        assume z in ( compactbelow x);

        then z in { v where v be Element of L : x >= v & v is compact } by WAYBEL_8:def 2;

        then

        consider z9 be Element of L such that

         A2: z9 = z and

         A3: x >= z9 and

         A4: z9 is compact;

        z9 <= y by A1, A3, ORDERS_2: 3;

        hence z in ( compactbelow y) by A2, A4, WAYBEL_8: 4;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL13:2

    

     Th2: for L be non empty reflexive RelStr holds for x be Element of L holds ( compactbelow x) is Subset of ( CompactSublatt L)

    proof

      let L be non empty reflexive RelStr;

      let x be Element of L;

      now

        let v be object;

        assume v in ( compactbelow x);

        then v in { z where z be Element of L : x >= z & z is compact } by WAYBEL_8:def 2;

        then ex v1 be Element of L st v1 = v & x >= v1 & v1 is compact;

        hence v in the carrier of ( CompactSublatt L) by WAYBEL_8:def 1;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: WAYBEL13:3

    

     Th3: for L be RelStr holds for S be SubRelStr of L holds for X be Subset of S holds X is Subset of L

    proof

      let L be RelStr;

      let S be SubRelStr of L;

      let X be Subset of S;

      the carrier of S c= the carrier of L by YELLOW_0:def 13;

      hence thesis by XBOOLE_1: 1;

    end;

    theorem :: WAYBEL13:4

    

     Th4: for L be with_suprema non empty reflexive transitive RelStr holds the carrier of L is Ideal of L

    proof

      let L be with_suprema non empty reflexive transitive RelStr;

      ( [#] L) is Ideal of L;

      hence thesis;

    end;

    theorem :: WAYBEL13:5

    

     Th5: for L1 be lower-bounded non empty reflexive antisymmetric RelStr holds for L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the RelStr of L2 & L1 is up-complete holds the carrier of ( CompactSublatt L1) = the carrier of ( CompactSublatt L2)

    proof

      let L1 be lower-bounded non empty reflexive antisymmetric RelStr;

      let L2 be non empty reflexive antisymmetric RelStr;

      assume that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: L1 is up-complete;

      now

        reconsider L29 = L2 as lower-bounded non empty reflexive antisymmetric RelStr by A1, YELLOW_0: 13;

        let x be object;

        assume

         A3: x in the carrier of ( CompactSublatt L2);

        then x is Element of ( CompactSublatt L29);

        then

        reconsider x2 = x as Element of L2 by YELLOW_0: 58;

        reconsider x1 = x2 as Element of L1 by A1;

        

         A4: x2 is compact by A3, WAYBEL_8:def 1;

        L2 is up-complete by A1, A2, WAYBEL_8: 15;

        then x1 is compact by A1, A4, WAYBEL_8: 9;

        hence x in the carrier of ( CompactSublatt L1) by WAYBEL_8:def 1;

      end;

      then

       A5: the carrier of ( CompactSublatt L2) c= the carrier of ( CompactSublatt L1);

      now

        let x be object;

        assume

         A6: x in the carrier of ( CompactSublatt L1);

        then

        reconsider x1 = x as Element of L1 by YELLOW_0: 58;

        reconsider x2 = x1 as Element of L2 by A1;

        x1 is compact by A6, WAYBEL_8:def 1;

        then x2 is compact by A1, A2, WAYBEL_8: 9;

        hence x in the carrier of ( CompactSublatt L2) by WAYBEL_8:def 1;

      end;

      then the carrier of ( CompactSublatt L1) c= the carrier of ( CompactSublatt L2);

      hence thesis by A5, XBOOLE_0:def 10;

    end;

    begin

    theorem :: WAYBEL13:6

    

     Th6: for L be algebraic lower-bounded LATTICE holds for S be CLSubFrame of L holds S is algebraic

    proof

      let L be algebraic lower-bounded LATTICE;

      let S be CLSubFrame of L;

       the RelStr of S = ( Image ( closure_op S)) by WAYBEL10: 18;

      then the RelStr of S is algebraic by WAYBEL_8: 24;

      hence thesis by WAYBEL_8: 17;

    end;

    theorem :: WAYBEL13:7

    

     Th7: for X,E be set holds for L be CLSubFrame of ( BoolePoset X) holds E in the carrier of ( CompactSublatt L) iff ex F be Element of ( BoolePoset X) st F is finite & E = ( meet { Y where Y be Element of L : F c= Y }) & F c= E

    proof

      let X,E be set;

      let L be CLSubFrame of ( BoolePoset X);

      

       A1: the carrier of L c= the carrier of ( BoolePoset X) by YELLOW_0:def 13;

      

       A2: L is complete LATTICE by YELLOW_2: 30;

      thus E in the carrier of ( CompactSublatt L) implies ex F be Element of ( BoolePoset X) st F is finite & E = ( meet { Y where Y be Element of L : F c= Y }) & F c= E

      proof

        

         A3: (( closure_op L) .: ( [#] ( CompactSublatt ( BoolePoset X)))) = ( [#] ( CompactSublatt ( Image ( closure_op L)))) by WAYBEL_8: 25

        .= ( [#] ( CompactSublatt the RelStr of L)) by WAYBEL10: 18

        .= the carrier of ( CompactSublatt the RelStr of L);

        assume E in the carrier of ( CompactSublatt L);

        then E in (( closure_op L) .: ( [#] ( CompactSublatt ( BoolePoset X)))) by A2, A3, Th5;

        then

        consider x be object such that

         A4: x in ( dom ( closure_op L)) and

         A5: x in ( [#] ( CompactSublatt ( BoolePoset X))) and

         A6: E = (( closure_op L) . x) by FUNCT_1:def 6;

        reconsider F = x as Element of ( BoolePoset X) by A4;

        ( id ( BoolePoset X)) <= ( closure_op L) by WAYBEL_1:def 14;

        then (( id ( BoolePoset X)) . F) <= (( closure_op L) . F) by YELLOW_2: 9;

        then F <= (( closure_op L) . F);

        then

         A7: F c= (( closure_op L) . F) by YELLOW_1: 2;

        (( closure_op L) . x) in ( rng ( closure_op L)) by A4, FUNCT_1:def 3;

        then (( closure_op L) . x) in the carrier of ( Image ( closure_op L)) by YELLOW_0:def 15;

        then (( closure_op L) . x) in the carrier of the RelStr of L by WAYBEL10: 18;

        then

         A8: (( closure_op L) . x) in { Y where Y be Element of L : F c= Y } by A7;

        take F;

        F is compact by A5, WAYBEL_8:def 1;

        hence F is finite by WAYBEL_8: 28;

        

         A9: (( uparrow F) /\ the carrier of L) c= { Y where Y be Element of L : F c= Y }

        proof

          let z be object;

          assume

           A10: z in (( uparrow F) /\ the carrier of L);

          then

          reconsider z9 = z as Element of ( BoolePoset X);

          z in ( uparrow F) by A10, XBOOLE_0:def 4;

          then F <= z9 by WAYBEL_0: 18;

          then

           A11: F c= z9 by YELLOW_1: 2;

          z in the carrier of L by A10, XBOOLE_0:def 4;

          hence thesis by A11;

        end;

        { Y where Y be Element of L : F c= Y } c= (( uparrow F) /\ the carrier of L)

        proof

          let z be object;

          assume z in { Y where Y be Element of L : F c= Y };

          then

          consider z9 be Element of L such that

           A12: z = z9 and

           A13: F c= z9;

          reconsider z1 = z9 as Element of ( BoolePoset X) by A1;

          F <= z1 by A13, YELLOW_1: 2;

          then z in ( uparrow F) by A12, WAYBEL_0: 18;

          hence thesis by A12, XBOOLE_0:def 4;

        end;

        then

         A14: (( uparrow F) /\ the carrier of L) = { Y where Y be Element of L : F c= Y } by A9, XBOOLE_0:def 10;

        

        thus

         A15: E = ( "/\" ((( uparrow F) /\ the carrier of L),( BoolePoset X))) by A6, WAYBEL10:def 5

        .= ( meet { Y where Y be Element of L : F c= Y }) by A8, A14, YELLOW_1: 20;

        now

          let v be object;

          assume

           A16: v in F;

          now

            let V be set;

            assume V in { Y where Y be Element of L : F c= Y };

            then ex V9 be Element of L st V = V9 & F c= V9;

            hence v in V by A16;

          end;

          hence v in E by A8, A15, SETFAM_1:def 1;

        end;

        hence thesis;

      end;

      thus (ex F be Element of ( BoolePoset X) st F is finite & E = ( meet { Y where Y be Element of L : F c= Y }) & F c= E) implies E in the carrier of ( CompactSublatt L)

      proof

        given F be Element of ( BoolePoset X) such that

         A17: F is finite and

         A18: E = ( meet { Y where Y be Element of L : F c= Y }) and F c= E;

        F is compact by A17, WAYBEL_8: 28;

        then

         A19: F in ( [#] ( CompactSublatt ( BoolePoset X))) by WAYBEL_8:def 1;

        

         A20: (( uparrow F) /\ the carrier of L) c= { Y where Y be Element of L : F c= Y }

        proof

          let z be object;

          assume

           A21: z in (( uparrow F) /\ the carrier of L);

          then

          reconsider z9 = z as Element of ( BoolePoset X);

          z in ( uparrow F) by A21, XBOOLE_0:def 4;

          then F <= z9 by WAYBEL_0: 18;

          then

           A22: F c= z9 by YELLOW_1: 2;

          z in the carrier of L by A21, XBOOLE_0:def 4;

          hence thesis by A22;

        end;

        { Y where Y be Element of L : F c= Y } c= (( uparrow F) /\ the carrier of L)

        proof

          let z be object;

          assume z in { Y where Y be Element of L : F c= Y };

          then

          consider z9 be Element of L such that

           A23: z = z9 and

           A24: F c= z9;

          reconsider z1 = z9 as Element of ( BoolePoset X) by A1;

          F <= z1 by A24, YELLOW_1: 2;

          then z in ( uparrow F) by A23, WAYBEL_0: 18;

          hence thesis by A23, XBOOLE_0:def 4;

        end;

        then

         A25: (( uparrow F) /\ the carrier of L) = { Y where Y be Element of L : F c= Y } by A20, XBOOLE_0:def 10;

        ( id ( BoolePoset X)) <= ( closure_op L) by WAYBEL_1:def 14;

        then (( id ( BoolePoset X)) . F) <= (( closure_op L) . F) by YELLOW_2: 9;

        then F <= (( closure_op L) . F);

        then

         A26: F c= (( closure_op L) . F) by YELLOW_1: 2;

        F in the carrier of ( BoolePoset X);

        then

         A27: F in ( dom ( closure_op L)) by FUNCT_2:def 1;

        then (( closure_op L) . F) in ( rng ( closure_op L)) by FUNCT_1:def 3;

        then (( closure_op L) . F) in the carrier of ( Image ( closure_op L)) by YELLOW_0:def 15;

        then (( closure_op L) . F) in the carrier of the RelStr of L by WAYBEL10: 18;

        then (( closure_op L) . F) in { Y where Y be Element of L : F c= Y } by A26;

        

        then E = ( "/\" ((( uparrow F) /\ the carrier of L),( BoolePoset X))) by A18, A25, YELLOW_1: 20

        .= (( closure_op L) . F) by WAYBEL10:def 5;

        then

         A28: E in (( closure_op L) .: ( [#] ( CompactSublatt ( BoolePoset X)))) by A27, A19, FUNCT_1:def 6;

        (( closure_op L) .: ( [#] ( CompactSublatt ( BoolePoset X)))) = ( [#] ( CompactSublatt ( Image ( closure_op L)))) by WAYBEL_8: 25

        .= ( [#] ( CompactSublatt the RelStr of L)) by WAYBEL10: 18

        .= the carrier of ( CompactSublatt the RelStr of L);

        hence thesis by A2, A28, Th5;

      end;

    end;

    theorem :: WAYBEL13:8

    

     Th8: for L be lower-bounded sup-Semilattice holds ( InclPoset ( Ids L)) is CLSubFrame of ( BoolePoset the carrier of L)

    proof

      let L be lower-bounded sup-Semilattice;

      now

        let x be object;

        assume x in ( Ids L);

        then x in the set of all X where X be Ideal of L by WAYBEL_0:def 23;

        then ex x9 be Ideal of L st x9 = x;

        hence x in ( bool the carrier of L);

      end;

      then ( Ids L) is Subset-Family of L by TARSKI:def 3;

      then

      reconsider InIdL = ( InclPoset ( Ids L)) as non empty full SubRelStr of ( BoolePoset the carrier of L) by YELLOW_1: 5;

      

       A1: for X be directed Subset of InIdL st X <> {} & ex_sup_of (X,( BoolePoset the carrier of L)) holds ( "\/" (X,( BoolePoset the carrier of L))) in the carrier of InIdL

      proof

        let X be directed Subset of InIdL;

        assume that

         A2: X <> {} and ex_sup_of (X,( BoolePoset the carrier of L));

        consider Y be object such that

         A3: Y in X by A2, XBOOLE_0:def 1;

        X is Subset of ( BoolePoset the carrier of L) by Th3;

        then

         A4: ( "\/" (X,( BoolePoset the carrier of L))) = ( union X) by YELLOW_1: 21;

        then

        reconsider uX = ( union X) as Subset of L by WAYBEL_8: 26;

        reconsider Y as set by TARSKI: 1;

        Y is Ideal of L by A3, YELLOW_2: 41;

        then ( Bottom L) in Y by WAYBEL_4: 21;

        then

        reconsider uX as non empty Subset of L by A3, TARSKI:def 4;

        now

          let z be object;

          assume z in X;

          then z is Ideal of L by YELLOW_2: 41;

          hence z in ( bool the carrier of L);

        end;

        then

         A5: X c= ( bool the carrier of L);

         A6:

        now

          let Y,Z be Subset of L;

          assume

           A7: Y in X & Z in X;

          then

          reconsider Y9 = Y, Z9 = Z as Element of InIdL;

          consider V9 be Element of InIdL such that

           A8: V9 in X and

           A9: Y9 <= V9 & Z9 <= V9 by A7, WAYBEL_0:def 1;

          reconsider V = V9 as Subset of L by YELLOW_2: 41;

          take V;

          thus V in X by A8;

          (Y9 "\/" Z9) <= V9 by A9, YELLOW_0: 22;

          then

           A10: (Y9 "\/" Z9) c= V9 by YELLOW_1: 3;

          (Y \/ Z) c= (Y9 "\/" Z9) by YELLOW_1: 6;

          hence (Y \/ Z) c= V by A10;

        end;

        (for Y be Subset of L st Y in X holds Y is lower) & for Y be Subset of L st Y in X holds Y is directed by YELLOW_2: 41;

        then uX is Ideal of L by A5, A6, WAYBEL_0: 26, WAYBEL_0: 46;

        then ( "\/" (X,( BoolePoset the carrier of L))) is Element of InIdL by A4, YELLOW_2: 41;

        hence thesis;

      end;

      for X be Subset of InIdL st ex_inf_of (X,( BoolePoset the carrier of L)) holds ( "/\" (X,( BoolePoset the carrier of L))) in the carrier of InIdL

      proof

        let X be Subset of InIdL;

        assume ex_inf_of (X,( BoolePoset the carrier of L));

        now

          per cases ;

            suppose

             A11: X is non empty;

            X is Subset of ( BoolePoset the carrier of L) by Th3;

            then

             A12: ( "/\" (X,( BoolePoset the carrier of L))) = ( meet X) by A11, YELLOW_1: 20;

            ( InclPoset ( Ids L)) = RelStr (# ( Ids L), ( RelIncl ( Ids L)) #) by YELLOW_1:def 1;

            then ( "/\" (X,( BoolePoset the carrier of L))) is Ideal of L by A11, A12, YELLOW_2: 45;

            then ( "/\" (X,( BoolePoset the carrier of L))) is Element of InIdL by YELLOW_2: 41;

            hence thesis;

          end;

            suppose

             A13: X is empty;

            ( "/\" ( {} ,( BoolePoset the carrier of L))) = ( Top ( BoolePoset the carrier of L)) by YELLOW_0:def 12

            .= the carrier of L by YELLOW_1: 19;

            then ( "/\" ( {} ,( BoolePoset the carrier of L))) is Ideal of L by Th4;

            then ( "/\" (X,( BoolePoset the carrier of L))) is Element of InIdL by A13, YELLOW_2: 41;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1, WAYBEL_0:def 4, YELLOW_0:def 18;

    end;

    registration

      let L be non empty reflexive transitive RelStr;

      cluster principal for Ideal of L;

      existence

      proof

        set x = the Element of L;

        take ( downarrow x);

        thus thesis by WAYBEL_0: 48;

      end;

    end

    theorem :: WAYBEL13:9

    

     Th9: for L be lower-bounded sup-Semilattice holds for X be non empty directed Subset of ( InclPoset ( Ids L)) holds ( sup X) = ( union X)

    proof

      let L be lower-bounded sup-Semilattice;

      let X be non empty directed Subset of ( InclPoset ( Ids L));

      consider z be object such that

       A1: z in X by XBOOLE_0:def 1;

      X c= the carrier of ( InclPoset ( Ids L));

      then

       A2: X c= ( Ids L) by YELLOW_1: 1;

      now

        let x be object;

        assume x in X;

        then x in ( Ids L) by A2;

        then x in the set of all Y where Y be Ideal of L by WAYBEL_0:def 23;

        then ex x1 be Ideal of L st x = x1;

        hence x in ( bool the carrier of L);

      end;

      then

       A3: X c= ( bool the carrier of L);

      now

        let Z be Subset of L;

        assume Z in X;

        then Z in ( Ids L) by A2;

        then Z in the set of all Y where Y be Ideal of L by WAYBEL_0:def 23;

        then ex Z1 be Ideal of L st Z = Z1;

        hence Z is lower;

      end;

      then

      reconsider unX = ( union X) as lower Subset of L by A3, WAYBEL_0: 26;

      reconsider z as set by TARSKI: 1;

      z in ( Ids L) by A2, A1;

      then z in the set of all Y where Y be Ideal of L by WAYBEL_0:def 23;

      then ex z1 be Ideal of L st z = z1;

      then ex v be object st v in z by XBOOLE_0:def 1;

      then

      reconsider unX as lower non empty Subset of L by A1, TARSKI:def 4;

       A4:

      now

        let V,Y be Subset of L;

        assume

         A5: V in X & Y in X;

        then

        reconsider V1 = V, Y1 = Y as Element of ( InclPoset ( Ids L));

        consider Z1 be Element of ( InclPoset ( Ids L)) such that

         A6: Z1 in X and

         A7: V1 <= Z1 & Y1 <= Z1 by A5, WAYBEL_0:def 1;

        Z1 in ( Ids L) by A2, A6;

        then Z1 in the set of all Y9 where Y9 be Ideal of L by WAYBEL_0:def 23;

        then ex Z2 be Ideal of L st Z1 = Z2;

        then

        reconsider Z = Z1 as Subset of L;

        take Z;

        thus Z in X by A6;

        V c= Z & Y c= Z by A7, YELLOW_1: 3;

        hence (V \/ Y) c= Z by XBOOLE_1: 8;

      end;

      now

        let Z be Subset of L;

        assume Z in X;

        then Z in ( Ids L) by A2;

        then Z in the set of all Y where Y be Ideal of L by WAYBEL_0:def 23;

        then ex Z1 be Ideal of L st Z = Z1;

        hence Z is directed;

      end;

      then

      reconsider unX as directed lower non empty Subset of L by A3, A4, WAYBEL_0: 46;

      reconsider unX as Element of ( InclPoset ( Ids L)) by YELLOW_2: 41;

      now

        let Y be set;

        assume

         A8: Y in X;

        then

        reconsider Y9 = Y as Element of ( InclPoset ( Ids L));

        ( sup X) is_>=_than X by YELLOW_0: 32;

        then Y9 <= ( sup X) by A8, LATTICE3:def 9;

        hence Y c= ( sup X) by YELLOW_1: 3;

      end;

      then ( union X) c= ( sup X) by ZFMISC_1: 76;

      then

       A9: unX <= ( sup X) by YELLOW_1: 3;

      for b be Element of ( InclPoset ( Ids L)) st b in X holds b <= unX by YELLOW_1: 3, ZFMISC_1: 74;

      then unX is_>=_than X by LATTICE3:def 9;

      then ( sup X) <= unX by YELLOW_0: 32;

      hence thesis by A9, ORDERS_2: 2;

    end;

    theorem :: WAYBEL13:10

    

     Th10: for S be lower-bounded sup-Semilattice holds ( InclPoset ( Ids S)) is algebraic

    proof

      let S be lower-bounded sup-Semilattice;

      set BS = ( BoolePoset the carrier of S);

      ( Ids S) c= ( bool the carrier of S)

      proof

        let x be object;

        assume x in ( Ids S);

        then x in the set of all X where X be Ideal of S by WAYBEL_0:def 23;

        then ex x1 be Ideal of S st x = x1;

        hence thesis;

      end;

      then

      reconsider InIdsS = ( InclPoset ( Ids S)) as non empty full SubRelStr of ( BoolePoset the carrier of S) by YELLOW_1: 5;

      

       A1: the carrier of InIdsS c= the carrier of BS by YELLOW_0:def 13;

      now

        let X be Subset of InIdsS;

        assume ex_inf_of (X,BS);

        now

          per cases ;

            suppose

             A2: X <> {} ;

            for x be object st x in X holds x in the carrier of BS by A1;

            then X c= the carrier of BS;

            

            then ( "/\" (X,BS)) = ( meet X) by A2, YELLOW_1: 20

            .= ( "/\" (X,InIdsS)) by A2, YELLOW_2: 46;

            hence ( "/\" (X,BS)) in the carrier of InIdsS;

          end;

            suppose

             A3: X = {} ;

            ( "/\" ( {} ,BS)) = ( Top BS) by YELLOW_0:def 12

            .= the carrier of S by YELLOW_1: 19

            .= ( [#] S)

            .= ( "/\" ( {} ,InIdsS)) by YELLOW_2: 47;

            hence ( "/\" (X,BS)) in the carrier of InIdsS by A3;

          end;

        end;

        hence ( "/\" (X,BS)) in the carrier of InIdsS;

      end;

      then

       A4: InIdsS is infs-inheriting by YELLOW_0:def 18;

      now

        let Y be directed Subset of InIdsS;

        assume that

         A5: Y <> {} and ex_sup_of (Y,BS);

        for x be object st x in Y holds x in the carrier of BS by A1;

        then Y c= the carrier of BS;

        

        then ( "\/" (Y,BS)) = ( union Y) by YELLOW_1: 21

        .= ( "\/" (Y,InIdsS)) by A5, Th9;

        hence ( "\/" (Y,BS)) in the carrier of InIdsS;

      end;

      then InIdsS is directed-sups-inheriting by WAYBEL_0:def 4;

      hence thesis by A4, Th6;

    end;

    theorem :: WAYBEL13:11

    

     Th11: for S be lower-bounded sup-Semilattice holds for x be Element of ( InclPoset ( Ids S)) holds x is compact iff x is principal Ideal of S

    proof

      let S be lower-bounded sup-Semilattice;

      reconsider InIdS = ( InclPoset ( Ids S)) as CLSubFrame of ( BoolePoset the carrier of S) by Th8;

      let x be Element of ( InclPoset ( Ids S));

      reconsider x9 = x as Ideal of S by YELLOW_2: 41;

      thus x is compact implies x is principal Ideal of S

      proof

        assume x is compact;

        then x in the carrier of ( CompactSublatt InIdS) by WAYBEL_8:def 1;

        then

        consider F be Element of ( BoolePoset the carrier of S) such that

         A1: F is finite and

         A2: x = ( meet { Y where Y be Element of InIdS : F c= Y }) and

         A3: F c= x by Th7;

        

         A4: F c= the carrier of S by WAYBEL_8: 26;

        ex y be Element of S st y in x9 & y is_>=_than x9

        proof

          reconsider F9 = F as Subset of S by WAYBEL_8: 26;

          reconsider F9 as Subset of S;

          reconsider y = ( sup F9) as Element of S;

          take y;

          now

            per cases ;

              suppose F9 <> {} ;

              hence y in x9 by A1, A3, WAYBEL_0: 42;

            end;

              suppose F9 = {} ;

              then y = ( Bottom S) by YELLOW_0:def 11;

              hence y in x9 by WAYBEL_4: 21;

            end;

          end;

          hence y in x9;

          now

            now

              let u be object;

              assume

               A5: u in F;

              then

              reconsider u9 = u as Element of S by A4;

               ex_sup_of (F9,S) by A1, A5, YELLOW_0: 54;

              then y is_>=_than F by YELLOW_0: 30;

              then u9 <= y by A5, LATTICE3:def 9;

              hence u in ( downarrow y) by WAYBEL_0: 17;

            end;

            then

             A6: F c= ( downarrow y);

            let b be Element of S;

            assume

             A7: b in x9;

            ( downarrow y) is Element of InIdS by YELLOW_2: 41;

            then ( downarrow y) in { Y where Y be Element of InIdS : F c= Y } by A6;

            then b in ( downarrow y) by A2, A7, SETFAM_1:def 1;

            hence b <= y by WAYBEL_0: 17;

          end;

          hence thesis by LATTICE3:def 9;

        end;

        hence thesis by WAYBEL_0:def 21;

      end;

      thus x is principal Ideal of S implies x is compact

      proof

        assume x is principal Ideal of S;

        then

        consider y be Element of S such that

         A8: y in x9 and

         A9: y is_>=_than x9 by WAYBEL_0:def 21;

        ex F be Element of ( BoolePoset the carrier of S) st F is finite & F c= x & x = ( meet { Y where Y be Element of InIdS : F c= Y })

        proof

          reconsider F = {y} as Element of ( BoolePoset the carrier of S) by WAYBEL_8: 26;

          take F;

          thus F is finite;

          for v be object st v in F holds v in x by A8, TARSKI:def 1;

          hence

           A10: F c= x;

           A11:

          now

            let z be object;

            thus z in x implies for Z be set holds Z in { Y where Y be Element of InIdS : F c= Y } implies z in Z

            proof

              assume

               A12: z in x;

              then

              reconsider z9 = z as Element of S by YELLOW_2: 42;

              

               A13: z9 <= y by A9, A12, LATTICE3:def 9;

              let Z be set;

              assume Z in { Y where Y be Element of InIdS : F c= Y };

              then

              consider Z1 be Element of InIdS such that

               A14: Z1 = Z & F c= Z1;

              Z1 is Ideal of S & y in F by TARSKI:def 1, YELLOW_2: 41;

              hence thesis by A14, A13, WAYBEL_0:def 19;

            end;

            thus (for Z be set holds Z in { Y where Y be Element of InIdS : F c= Y } implies z in Z) implies z in x

            proof

              assume

               A15: for Z be set holds Z in { Y where Y be Element of InIdS : F c= Y } implies z in Z;

              x in { Y where Y be Element of InIdS : F c= Y } by A10;

              hence thesis by A15;

            end;

          end;

          ( [#] S) is Element of InIdS by YELLOW_2: 41;

          then ( [#] S) in { Y where Y be Element of InIdS : F c= Y };

          hence thesis by A11, SETFAM_1:def 1;

        end;

        then x in the carrier of ( CompactSublatt InIdS) by Th7;

        hence thesis by WAYBEL_8:def 1;

      end;

    end;

    theorem :: WAYBEL13:12

    

     Th12: for S be lower-bounded sup-Semilattice holds for x be Element of ( InclPoset ( Ids S)) holds x is compact iff ex a be Element of S st x = ( downarrow a)

    proof

      let S be lower-bounded sup-Semilattice;

      let x be Element of ( InclPoset ( Ids S));

      thus x is compact implies ex a be Element of S st x = ( downarrow a)

      proof

        assume x is compact;

        then x is principal Ideal of S by Th11;

        hence thesis by WAYBEL_0: 48;

      end;

      thus (ex a be Element of S st x = ( downarrow a)) implies x is compact by WAYBEL_0: 48, Th11;

    end;

    theorem :: WAYBEL13:13

    for L be lower-bounded sup-Semilattice holds for f be Function of L, ( CompactSublatt ( InclPoset ( Ids L))) st for x be Element of L holds (f . x) = ( downarrow x) holds f is isomorphic

    proof

      let L be lower-bounded sup-Semilattice;

      let f be Function of L, ( CompactSublatt ( InclPoset ( Ids L)));

      assume

       A1: for x be Element of L holds (f . x) = ( downarrow x);

      

       A2: for x,y be Element of L holds x <= y iff (f . x) <= (f . y)

      proof

        let x,y be Element of L;

        reconsider fx = (f . x) as Element of ( InclPoset ( Ids L)) by YELLOW_0: 58;

        reconsider fy = (f . y) as Element of ( InclPoset ( Ids L)) by YELLOW_0: 58;

        thus x <= y implies (f . x) <= (f . y)

        proof

          assume x <= y;

          then ( downarrow x) c= ( downarrow y) by WAYBEL_0: 21;

          then (f . x) c= ( downarrow y) by A1;

          then fx c= fy by A1;

          then fx <= fy by YELLOW_1: 3;

          hence thesis by YELLOW_0: 60;

        end;

        x <= x;

        then

         A3: x in ( downarrow x) by WAYBEL_0: 17;

        thus (f . x) <= (f . y) implies x <= y

        proof

          assume (f . x) <= (f . y);

          then fx <= fy by YELLOW_0: 59;

          then fx c= fy by YELLOW_1: 3;

          then (f . x) c= ( downarrow y) by A1;

          then ( downarrow x) c= ( downarrow y) by A1;

          hence thesis by A3, WAYBEL_0: 17;

        end;

      end;

      now

        let y be object;

        assume

         A4: y in the carrier of ( CompactSublatt ( InclPoset ( Ids L)));

        the carrier of ( CompactSublatt ( InclPoset ( Ids L))) c= the carrier of ( InclPoset ( Ids L)) by YELLOW_0:def 13;

        then

        reconsider y9 = y as Element of ( InclPoset ( Ids L)) by A4;

        y9 is compact by A4, WAYBEL_8:def 1;

        then

        consider x be Element of L such that

         A5: y9 = ( downarrow x) by Th12;

        reconsider x9 = x as object;

        take x9;

        thus x9 in the carrier of L;

        thus y = (f . x9) by A1, A5;

      end;

      then

       A6: ( rng f) = the carrier of ( CompactSublatt ( InclPoset ( Ids L))) by FUNCT_2: 10;

      now

        let x,y be Element of L;

        assume (f . x) = (f . y);

        then (f . x) = ( downarrow y) by A1;

        then ( downarrow x) = ( downarrow y) by A1;

        hence x = y by WAYBEL_0: 19;

      end;

      then f is one-to-one by WAYBEL_1:def 1;

      hence thesis by A6, A2, WAYBEL_0: 66;

    end;

    theorem :: WAYBEL13:14

    for S be lower-bounded LATTICE holds ( InclPoset ( Ids S)) is arithmetic

    proof

      let S be lower-bounded LATTICE;

      now

        let x,y be Element of ( CompactSublatt ( InclPoset ( Ids S)));

        reconsider x1 = x, y1 = y as Element of ( InclPoset ( Ids S)) by YELLOW_0: 58;

        x1 is compact by WAYBEL_8:def 1;

        then

        consider a be Element of S such that

         A1: x1 = ( downarrow a) by Th12;

        y1 is compact by WAYBEL_8:def 1;

        then

        consider b be Element of S such that

         A2: y1 = ( downarrow b) by Th12;

        ( Bottom S) <= b by YELLOW_0: 44;

        then

         A3: ( Bottom S) in ( downarrow b) by WAYBEL_0: 17;

        ( Bottom S) <= a by YELLOW_0: 44;

        then ( Bottom S) in ( downarrow a) by WAYBEL_0: 17;

        then

        reconsider xy = (( downarrow a) /\ ( downarrow b)) as non empty Subset of S by A3, XBOOLE_0:def 4;

        reconsider xy as lower non empty Subset of S by WAYBEL_0: 27;

        reconsider xy as lower directed non empty Subset of S by WAYBEL_0: 44;

        xy is Ideal of S;

        then (( downarrow a) /\ ( downarrow b)) in the set of all X where X be Ideal of S;

        then (( downarrow a) /\ ( downarrow b)) in ( Ids S) by WAYBEL_0:def 23;

        then (x1 "/\" y1) = (( downarrow a) /\ ( downarrow b)) by A1, A2, YELLOW_1: 9;

        then

        reconsider z1 = (( downarrow a) /\ ( downarrow b)) as Element of ( InclPoset ( Ids S));

        z1 c= y1 by A2, XBOOLE_1: 17;

        then

         A4: z1 <= y1 by YELLOW_1: 3;

        

         A5: ( downarrow (a "/\" b)) c= (( downarrow a) /\ ( downarrow b))

        proof

          let v be object;

          assume

           A6: v in ( downarrow (a "/\" b));

          then

          reconsider v1 = v as Element of S;

          

           A7: v1 <= (a "/\" b) by A6, WAYBEL_0: 17;

          (a "/\" b) <= b by YELLOW_0: 23;

          then v1 <= b by A7, ORDERS_2: 3;

          then

           A8: v in ( downarrow b) by WAYBEL_0: 17;

          (a "/\" b) <= a by YELLOW_0: 23;

          then v1 <= a by A7, ORDERS_2: 3;

          then v in ( downarrow a) by WAYBEL_0: 17;

          hence thesis by A8, XBOOLE_0:def 4;

        end;

        (( downarrow a) /\ ( downarrow b)) c= ( downarrow (a "/\" b))

        proof

          let v be object;

          assume

           A9: v in (( downarrow a) /\ ( downarrow b));

          then

          reconsider v1 = v as Element of S;

          v in ( downarrow b) by A9, XBOOLE_0:def 4;

          then

           A10: v1 <= b by WAYBEL_0: 17;

          v in ( downarrow a) by A9, XBOOLE_0:def 4;

          then v1 <= a by WAYBEL_0: 17;

          then v1 <= (a "/\" b) by A10, YELLOW_0: 23;

          hence thesis by WAYBEL_0: 17;

        end;

        then z1 = ( downarrow (a "/\" b)) by A5, XBOOLE_0:def 10;

        then z1 is compact by Th12;

        then

        reconsider z = z1 as Element of ( CompactSublatt ( InclPoset ( Ids S))) by WAYBEL_8:def 1;

        take z;

        z1 c= x1 by A1, XBOOLE_1: 17;

        then z1 <= x1 by YELLOW_1: 3;

        hence z <= x & z <= y by A4, YELLOW_0: 60;

        let v be Element of ( CompactSublatt ( InclPoset ( Ids S)));

        reconsider v1 = v as Element of ( InclPoset ( Ids S)) by YELLOW_0: 58;

        assume that

         A11: v <= x and

         A12: v <= y;

        v1 <= y1 by A12, YELLOW_0: 59;

        then

         A13: v1 c= y1 by YELLOW_1: 3;

        v1 <= x1 by A11, YELLOW_0: 59;

        then v1 c= x1 by YELLOW_1: 3;

        then v1 c= z1 by A1, A2, A13, XBOOLE_1: 19;

        then v1 <= z1 by YELLOW_1: 3;

        hence v <= z by YELLOW_0: 60;

      end;

      then

       A14: ( CompactSublatt ( InclPoset ( Ids S))) is with_infima by LATTICE3:def 11;

      ( InclPoset ( Ids S)) is algebraic by Th10;

      hence thesis by A14, WAYBEL_8: 19;

    end;

    theorem :: WAYBEL13:15

    

     Th15: for L be lower-bounded sup-Semilattice holds ( CompactSublatt L) is lower-bounded sup-Semilattice

    proof

      let L be lower-bounded sup-Semilattice;

      ex x be Element of ( CompactSublatt L) st x is_<=_than the carrier of ( CompactSublatt L)

      proof

        reconsider x = ( Bottom L) as Element of ( CompactSublatt L) by WAYBEL_8: 3;

        take x;

        now

          let a be Element of ( CompactSublatt L);

          

           A1: the carrier of ( CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;

          assume a in the carrier of ( CompactSublatt L);

          reconsider a9 = a as Element of L by A1;

          ( Bottom L) <= a9 by YELLOW_0: 44;

          hence x <= a by YELLOW_0: 60;

        end;

        hence thesis by LATTICE3:def 8;

      end;

      hence thesis by YELLOW_0:def 4;

    end;

    theorem :: WAYBEL13:16

    

     Th16: for L be algebraic lower-bounded sup-Semilattice holds for f be Function of L, ( InclPoset ( Ids ( CompactSublatt L))) st for x be Element of L holds (f . x) = ( compactbelow x) holds f is isomorphic

    proof

      let L be algebraic lower-bounded sup-Semilattice;

      let f be Function of L, ( InclPoset ( Ids ( CompactSublatt L)));

      assume

       A1: for x be Element of L holds (f . x) = ( compactbelow x);

       A2:

      now

        let x,y be Element of L;

        thus x <= y implies (f . x) <= (f . y)

        proof

          assume x <= y;

          then ( compactbelow x) c= ( compactbelow y) by Th1;

          then (f . x) c= ( compactbelow y) by A1;

          then (f . x) c= (f . y) by A1;

          hence thesis by YELLOW_1: 3;

        end;

        thus (f . x) <= (f . y) implies x <= y

        proof

          assume (f . x) <= (f . y);

          then (f . x) c= (f . y) by YELLOW_1: 3;

          then (f . x) c= ( compactbelow y) by A1;

          then

           A3: ( compactbelow x) c= ( compactbelow y) by A1;

           ex_sup_of (( compactbelow x),L) & ex_sup_of (( compactbelow y),L) by YELLOW_0: 17;

          then ( sup ( compactbelow x)) <= ( sup ( compactbelow y)) by A3, YELLOW_0: 34;

          then ( sup ( compactbelow x)) <= y by WAYBEL_8:def 3;

          hence thesis by WAYBEL_8:def 3;

        end;

      end;

      now

        let y be object;

        assume y in the carrier of ( InclPoset ( Ids ( CompactSublatt L)));

        then

        reconsider y9 = y as Ideal of ( CompactSublatt L) by YELLOW_2: 41;

        reconsider y1 = y9 as non empty Subset of L by Th3;

        reconsider y1 as non empty directed Subset of L by YELLOW_2: 7;

        set x = ( sup y1);

        reconsider x9 = x as object;

        take x9;

        thus x9 in the carrier of L;

        

         A4: ( compactbelow x) c= y9

        proof

          let d be object;

          assume d in ( compactbelow x);

          then d in { v where v be Element of L : x >= v & v is compact } by WAYBEL_8:def 2;

          then

          consider d1 be Element of L such that

           A5: d1 = d and

           A6: d1 <= x and

           A7: d1 is compact;

          reconsider d9 = d1 as Element of ( CompactSublatt L) by A7, WAYBEL_8:def 1;

          d1 << d1 by A7, WAYBEL_3:def 2;

          then

          consider z be Element of L such that

           A8: z in y1 and

           A9: d1 <= z by A6, WAYBEL_3:def 1;

          reconsider z9 = z as Element of ( CompactSublatt L) by A8;

          d9 <= z9 by A9, YELLOW_0: 60;

          hence thesis by A5, A8, WAYBEL_0:def 19;

        end;

        y9 c= ( compactbelow x)

        proof

          let d be object;

          assume

           A10: d in y9;

          then

          reconsider d1 = d as Element of ( CompactSublatt L);

          reconsider d9 = d1 as Element of L by YELLOW_0: 58;

          y9 is_<=_than ( sup y1) by YELLOW_0: 32;

          then d9 is compact & d9 <= x by A10, LATTICE3:def 9, WAYBEL_8:def 1;

          hence thesis by WAYBEL_8: 4;

        end;

        

        hence y = ( compactbelow x) by A4, XBOOLE_0:def 10

        .= (f . x9) by A1;

      end;

      then

       A11: ( rng f) = the carrier of ( InclPoset ( Ids ( CompactSublatt L))) by FUNCT_2: 10;

      now

        let x,y be Element of L;

        assume (f . x) = (f . y);

        then (f . x) = ( compactbelow y) by A1;

        then ( compactbelow x) = ( compactbelow y) by A1;

        then ( sup ( compactbelow x)) = y by WAYBEL_8:def 3;

        hence x = y by WAYBEL_8:def 3;

      end;

      then f is one-to-one by WAYBEL_1:def 1;

      hence thesis by A11, A2, WAYBEL_0: 66;

    end;

    theorem :: WAYBEL13:17

    for L be algebraic lower-bounded sup-Semilattice holds for x be Element of L holds ( compactbelow x) is principal Ideal of ( CompactSublatt L) iff x is compact

    proof

      let L be algebraic lower-bounded sup-Semilattice;

      let x be Element of L;

      thus ( compactbelow x) is principal Ideal of ( CompactSublatt L) implies x is compact

      proof

        assume ( compactbelow x) is principal Ideal of ( CompactSublatt L);

        then

        consider y be Element of ( CompactSublatt L) such that

         A1: y in ( compactbelow x) and

         A2: y is_>=_than ( compactbelow x) by WAYBEL_0:def 21;

        reconsider y9 = y as Element of L by YELLOW_0: 58;

        ( compactbelow x) is Subset of ( CompactSublatt L) by Th2;

        then y9 is_>=_than ( compactbelow x) by A2, YELLOW_0: 62;

        then y9 >= ( sup ( compactbelow x)) by YELLOW_0: 32;

        then

         A3: x <= y9 by WAYBEL_8:def 3;

        y9 <= x & y9 is compact by A1, WAYBEL_8: 4;

        hence thesis by A3, ORDERS_2: 2;

      end;

      thus x is compact implies ( compactbelow x) is principal Ideal of ( CompactSublatt L)

      proof

        reconsider I = ( compactbelow x) as non empty Subset of ( CompactSublatt L) by Th2;

        assume

         A4: x is compact;

        then

        reconsider x9 = x as Element of ( CompactSublatt L) by WAYBEL_8:def 1;

        ( compactbelow x) is non empty directed Subset of L by WAYBEL_8:def 4;

        then

        reconsider I as non empty directed Subset of ( CompactSublatt L) by WAYBEL10: 23;

        now

          let y,z be Element of ( CompactSublatt L);

          reconsider y9 = y, z9 = z as Element of L by YELLOW_0: 58;

          assume y in I & z <= y;

          then y9 <= x & z9 <= y9 by WAYBEL_8: 4, YELLOW_0: 59;

          then

           A5: z9 <= x by ORDERS_2: 3;

          z9 is compact by WAYBEL_8:def 1;

          hence z in I by A5, WAYBEL_8: 4;

        end;

        then

        reconsider I as Ideal of ( CompactSublatt L) by WAYBEL_0:def 19;

        ( sup ( compactbelow x)) is_>=_than ( compactbelow x) by YELLOW_0: 32;

        then x is_>=_than I by WAYBEL_8:def 3;

        then

         A6: x9 is_>=_than I by YELLOW_0: 61;

        x <= x;

        then x9 in I by A4, WAYBEL_8: 4;

        hence thesis by A6, WAYBEL_0:def 21;

      end;

    end;

    begin

    theorem :: WAYBEL13:18

    

     Th18: for L1,L2 be non empty RelStr holds for X be Subset of L1, x be Element of L1 holds for f be Function of L1, L2 st f is isomorphic holds x is_<=_than X iff (f . x) is_<=_than (f .: X)

    proof

      let L1,L2 be non empty RelStr;

      let X be Subset of L1;

      let x be Element of L1;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      hence x is_<=_than X implies (f . x) is_<=_than (f .: X) by YELLOW_2: 13;

      thus (f . x) is_<=_than (f .: X) implies x is_<=_than X

      proof

        reconsider g = (f " ) as Function of L2, L1 by A1, WAYBEL_0: 67;

        assume

         A2: (f . x) is_<=_than (f .: X);

        g is isomorphic by A1, WAYBEL_0: 68;

        then

         A3: (g . (f . x)) is_<=_than (g .: (f .: X)) by A2, YELLOW_2: 13;

        

         A4: (f " (f .: X)) c= X by A1, FUNCT_1: 82;

        X c= the carrier of L1;

        then X c= ( dom f) by FUNCT_2:def 1;

        then

         A5: X c= (f " (f .: X)) by FUNCT_1: 76;

        x in the carrier of L1;

        then

         A6: x in ( dom f) by FUNCT_2:def 1;

        (g .: (f .: X)) = (f " (f .: X)) by A1, FUNCT_1: 85

        .= X by A4, A5, XBOOLE_0:def 10;

        hence thesis by A1, A6, A3, FUNCT_1: 34;

      end;

    end;

    theorem :: WAYBEL13:19

    

     Th19: for L1,L2 be non empty RelStr holds for X be Subset of L1, x be Element of L1 holds for f be Function of L1, L2 st f is isomorphic holds x is_>=_than X iff (f . x) is_>=_than (f .: X)

    proof

      let L1,L2 be non empty RelStr;

      let X be Subset of L1;

      let x be Element of L1;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      hence x is_>=_than X implies (f . x) is_>=_than (f .: X) by YELLOW_2: 14;

      thus (f . x) is_>=_than (f .: X) implies x is_>=_than X

      proof

        reconsider g = (f " ) as Function of L2, L1 by A1, WAYBEL_0: 67;

        assume

         A2: (f . x) is_>=_than (f .: X);

        g is isomorphic by A1, WAYBEL_0: 68;

        then

         A3: (g . (f . x)) is_>=_than (g .: (f .: X)) by A2, YELLOW_2: 14;

        

         A4: (f " (f .: X)) c= X by A1, FUNCT_1: 82;

        X c= the carrier of L1;

        then X c= ( dom f) by FUNCT_2:def 1;

        then

         A5: X c= (f " (f .: X)) by FUNCT_1: 76;

        x in the carrier of L1;

        then

         A6: x in ( dom f) by FUNCT_2:def 1;

        (g .: (f .: X)) = (f " (f .: X)) by A1, FUNCT_1: 85

        .= X by A4, A5, XBOOLE_0:def 10;

        hence thesis by A1, A6, A3, FUNCT_1: 34;

      end;

    end;

    theorem :: WAYBEL13:20

    

     Th20: for L1,L2 be non empty antisymmetric RelStr holds for f be Function of L1, L2 holds f is isomorphic implies f is infs-preserving sups-preserving

    proof

      let L1,L2 be non empty antisymmetric RelStr;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      then

       A2: ( rng f) = the carrier of L2 by WAYBEL_0: 66;

      now

        let X be Subset of L1;

        now

          assume

           A3: ex_inf_of (X,L1);

          then

          consider a be Element of L1 such that

           A4: X is_>=_than a and

           A5: for b be Element of L1 st X is_>=_than b holds a >= b by YELLOW_0: 16;

           A6:

          now

            let c be Element of L2;

            consider e be object such that

             A7: e in ( dom f) and

             A8: c = (f . e) by A2, FUNCT_1:def 3;

            reconsider e as Element of L1 by A7;

            assume (f .: X) is_>=_than c;

            then X is_>=_than e by A1, A8, Th18;

            then a >= e by A5;

            hence (f . a) >= c by A1, A8, WAYBEL_0: 66;

          end;

          (f .: X) is_>=_than (f . a) by A1, A4, Th18;

          hence ex_inf_of ((f .: X),L2) by A6, YELLOW_0: 16;

           A9:

          now

            let b be Element of L2;

            consider v be object such that

             A10: v in ( dom f) and

             A11: b = (f . v) by A2, FUNCT_1:def 3;

            reconsider v as Element of L1 by A10;

            assume b is_<=_than (f .: X);

            then v is_<=_than X by A1, A11, Th18;

            then ( inf X) >= v by A3, YELLOW_0: 31;

            hence (f . ( inf X)) >= b by A1, A11, WAYBEL_0: 66;

          end;

          ( inf X) is_<=_than X by A3, YELLOW_0: 31;

          then (f . ( inf X)) is_<=_than (f .: X) by A1, Th18;

          hence ( inf (f .: X)) = (f . ( inf X)) by A9, YELLOW_0: 31;

        end;

        hence f preserves_inf_of X by WAYBEL_0:def 30;

      end;

      hence f is infs-preserving by WAYBEL_0:def 32;

      now

        let X be Subset of L1;

        now

          assume

           A12: ex_sup_of (X,L1);

          then

          consider a be Element of L1 such that

           A13: X is_<=_than a and

           A14: for b be Element of L1 st X is_<=_than b holds a <= b by YELLOW_0: 15;

           A15:

          now

            let c be Element of L2;

            consider e be object such that

             A16: e in ( dom f) and

             A17: c = (f . e) by A2, FUNCT_1:def 3;

            reconsider e as Element of L1 by A16;

            assume (f .: X) is_<=_than c;

            then X is_<=_than e by A1, A17, Th19;

            then a <= e by A14;

            hence (f . a) <= c by A1, A17, WAYBEL_0: 66;

          end;

          (f .: X) is_<=_than (f . a) by A1, A13, Th19;

          hence ex_sup_of ((f .: X),L2) by A15, YELLOW_0: 15;

           A18:

          now

            let b be Element of L2;

            consider v be object such that

             A19: v in ( dom f) and

             A20: b = (f . v) by A2, FUNCT_1:def 3;

            reconsider v as Element of L1 by A19;

            assume b is_>=_than (f .: X);

            then v is_>=_than X by A1, A20, Th19;

            then ( sup X) <= v by A12, YELLOW_0: 30;

            hence (f . ( sup X)) <= b by A1, A20, WAYBEL_0: 66;

          end;

          ( sup X) is_>=_than X by A12, YELLOW_0: 30;

          then (f . ( sup X)) is_>=_than (f .: X) by A1, Th19;

          hence ( sup (f .: X)) = (f . ( sup X)) by A18, YELLOW_0: 30;

        end;

        hence f preserves_sup_of X by WAYBEL_0:def 31;

      end;

      hence thesis by WAYBEL_0:def 33;

    end;

    registration

      let L1,L2 be non empty antisymmetric RelStr;

      cluster isomorphic -> infs-preserving sups-preserving for Function of L1, L2;

      coherence by Th20;

    end

    theorem :: WAYBEL13:21

    

     Th21: for L1,L2,L3 be non empty transitive antisymmetric RelStr holds for f be Function of L1, L2 st f is infs-preserving holds L2 is full infs-inheriting SubRelStr of L3 & L3 is complete implies ex g be Function of L1, L3 st f = g & g is infs-preserving

    proof

      let L1,L2,L3 be non empty transitive antisymmetric RelStr;

      let f be Function of L1, L2;

      assume that

       A1: f is infs-preserving and

       A2: L2 is full infs-inheriting SubRelStr of L3 and

       A3: L3 is complete;

      the carrier of L2 c= the carrier of L3 by A2, YELLOW_0:def 13;

      then

      reconsider g = f as Function of L1, L3 by FUNCT_2: 7;

      take g;

      thus f = g;

      now

        let X be Subset of L1;

        now

          

           A4: f preserves_inf_of X by A1, WAYBEL_0:def 32;

          assume

           A5: ex_inf_of (X,L1);

          thus

           A6: ex_inf_of ((g .: X),L3) by A3, YELLOW_0: 17;

          then ( "/\" ((f .: X),L3)) in the carrier of L2 by A2, YELLOW_0:def 18;

          

          hence ( inf (g .: X)) = ( inf (f .: X)) by A2, A6, YELLOW_0: 63

          .= (g . ( inf X)) by A5, A4, WAYBEL_0:def 30;

        end;

        hence g preserves_inf_of X by WAYBEL_0:def 30;

      end;

      hence thesis by WAYBEL_0:def 32;

    end;

    theorem :: WAYBEL13:22

    

     Th22: for L1,L2,L3 be non empty transitive antisymmetric RelStr holds for f be Function of L1, L2 st f is monotone directed-sups-preserving holds L2 is full directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g be Function of L1, L3 st f = g & g is directed-sups-preserving

    proof

      let L1,L2,L3 be non empty transitive antisymmetric RelStr;

      let f be Function of L1, L2;

      assume that

       A1: f is monotone directed-sups-preserving and

       A2: L2 is full directed-sups-inheriting SubRelStr of L3 and

       A3: L3 is complete;

      the carrier of L2 c= the carrier of L3 by A2, YELLOW_0:def 13;

      then

      reconsider g = f as Function of L1, L3 by FUNCT_2: 7;

      take g;

      thus f = g;

      now

        let X be Subset of L1;

        assume

         A4: X is non empty directed;

        then

        consider d be object such that

         A5: d in X by XBOOLE_0:def 1;

        d in the carrier of L1 by A5;

        then d in ( dom f) by FUNCT_2:def 1;

        then (f . d) in (f .: X) by A5, FUNCT_1:def 6;

        then

         A6: (f .: X) is non empty directed by A1, A4, YELLOW_2: 15;

        now

          

           A7: f preserves_sup_of X by A1, A4, WAYBEL_0:def 37;

          assume

           A8: ex_sup_of (X,L1);

          thus ex_sup_of ((g .: X),L3) by A3, YELLOW_0: 17;

          

          hence ( sup (g .: X)) = ( sup (f .: X)) by A2, A6, WAYBEL_0: 7

          .= (g . ( sup X)) by A8, A7, WAYBEL_0:def 31;

        end;

        hence g preserves_sup_of X by WAYBEL_0:def 31;

      end;

      hence thesis by WAYBEL_0:def 37;

    end;

    theorem :: WAYBEL13:23

    

     Th23: for L be lower-bounded sup-Semilattice holds ( InclPoset ( Ids ( CompactSublatt L))) is CLSubFrame of ( BoolePoset the carrier of ( CompactSublatt L))

    proof

      let L be lower-bounded sup-Semilattice;

      ( CompactSublatt L) is lower-bounded sup-Semilattice by Th15;

      hence thesis by Th8;

    end;

    theorem :: WAYBEL13:24

    

     Th24: for L be algebraic lower-bounded LATTICE holds ex g be Function of L, ( BoolePoset the carrier of ( CompactSublatt L)) st g is infs-preserving & g is directed-sups-preserving & g is one-to-one & for x be Element of L holds (g . x) = ( compactbelow x)

    proof

      let L be algebraic lower-bounded LATTICE;

      deffunc F( Element of L) = ( compactbelow $1);

      

       A1: for y be Element of L holds F(y) is Element of ( InclPoset ( Ids ( CompactSublatt L)))

      proof

        let y be Element of L;

        reconsider comy = ( compactbelow y) as non empty directed Subset of L by WAYBEL_8:def 4;

        reconsider comy as non empty Subset of ( CompactSublatt L) by Th2;

        reconsider comy as non empty directed Subset of ( CompactSublatt L) by WAYBEL10: 23;

        now

          let x1,z1 be Element of ( CompactSublatt L);

          reconsider x2 = x1, z2 = z1 as Element of L by YELLOW_0: 58;

          assume x1 in comy & z1 <= x1;

          then x2 <= y & z2 <= x2 by WAYBEL_8: 4, YELLOW_0: 59;

          then

           A2: z2 <= y by ORDERS_2: 3;

          z2 is compact by WAYBEL_8:def 1;

          hence z1 in comy by A2, WAYBEL_8: 4;

        end;

        then comy is lower by WAYBEL_0:def 19;

        hence thesis by YELLOW_2: 41;

      end;

      consider g1 be Function of L, ( InclPoset ( Ids ( CompactSublatt L))) such that

       A3: for y be Element of L holds (g1 . y) = F(y) from FUNCT_2:sch 9( A1);

      now

        let k be object;

        assume k in the carrier of ( InclPoset ( Ids ( CompactSublatt L)));

        then k is Ideal of ( CompactSublatt L) by YELLOW_2: 41;

        then k is Element of ( BoolePoset the carrier of ( CompactSublatt L)) by WAYBEL_8: 26;

        hence k in the carrier of ( BoolePoset the carrier of ( CompactSublatt L));

      end;

      then the carrier of ( InclPoset ( Ids ( CompactSublatt L))) c= the carrier of ( BoolePoset the carrier of ( CompactSublatt L));

      then

      reconsider g = g1 as Function of L, ( BoolePoset the carrier of ( CompactSublatt L)) by FUNCT_2: 7;

      take g;

      

       A4: g1 is isomorphic by A3, Th16;

      

       A5: ( InclPoset ( Ids ( CompactSublatt L))) is full infs-inheriting directed-sups-inheriting SubRelStr of ( BoolePoset the carrier of ( CompactSublatt L)) by Th23;

      then ex g2 be Function of L, ( BoolePoset the carrier of ( CompactSublatt L)) st g1 = g2 & g2 is infs-preserving by A4, Th21;

      hence g is infs-preserving;

      ex g3 be Function of L, ( BoolePoset the carrier of ( CompactSublatt L)) st g1 = g3 & g3 is directed-sups-preserving by A4, A5, Th22;

      hence g is directed-sups-preserving;

      thus g is one-to-one by A4;

      let x be Element of L;

      thus thesis by A3;

    end;

    theorem :: WAYBEL13:25

    for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is algebraic lower-bounded LATTICE holds ( product J) is algebraic lower-bounded LATTICE

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

      assume

       A1: for i be Element of I holds (J . i) is algebraic lower-bounded LATTICE;

      then

       A2: for i be Element of I holds (J . i) is complete LATTICE;

      then

      reconsider L = ( product J) as non empty lower-bounded LATTICE by WAYBEL_3: 31;

      for i be Element of I holds (J . i) is antisymmetric by A1;

      then

       A3: ( product J) is antisymmetric by WAYBEL_3: 30;

      now

        let x be Element of ( product J);

        

         A4: for i be Element of I holds ( sup ( compactbelow (x . i))) = (( sup ( compactbelow x)) . i)

        proof

          let i be Element of I;

          

           A5: ( compactbelow (x . i)) c= ( pi (( compactbelow x),i))

          proof

            deffunc G( Element of I) = ( Bottom (J . $1));

            defpred C[ set] means $1 = i;

            let v be object;

            assume v in ( compactbelow (x . i));

            then v in { y where y be Element of (J . i) : (x . i) >= y & y is compact } by WAYBEL_8:def 2;

            then

            consider v1 be Element of (J . i) such that

             A6: v1 = v and

             A7: (x . i) >= v1 and

             A8: v1 is compact;

            deffunc F( set) = v1;

            consider f be Function such that

             A9: ( dom f) = I and

             A10: for j be Element of I holds ( C[j] implies (f . j) = F(j)) & ( not C[j] implies (f . j) = G(j)) from PARTFUN1:sch 4;

            

             A11: (f . i) = v1 by A10;

            now

              let k be Element of I;

              now

                per cases ;

                  suppose k = i;

                  hence (f . k) is Element of (J . k) by A10;

                end;

                  suppose k <> i;

                  then (f . k) = ( Bottom (J . k)) by A10;

                  hence (f . k) is Element of (J . k);

                end;

              end;

              hence (f . k) is Element of (J . k);

            end;

            then

            reconsider f as Element of ( product J) by A9, WAYBEL_3: 27;

            now

              let k be Element of I;

              

               A12: (J . k) is algebraic lower-bounded LATTICE by A1;

              now

                per cases ;

                  suppose k = i;

                  hence (f . k) <= (x . k) by A7, A10;

                end;

                  suppose k <> i;

                  then (f . k) = ( Bottom (J . k)) by A10;

                  hence (f . k) <= (x . k) by A12, YELLOW_0: 44;

                end;

              end;

              hence (f . k) <= (x . k);

            end;

            then

             A13: f <= x by WAYBEL_3: 28;

             A14:

            now

              let k be Element of I;

              

               A15: (J . k) is algebraic lower-bounded LATTICE by A1;

              now

                per cases ;

                  suppose

                   A16: k = i;

                  then (f . k) = v1 by A10;

                  hence (f . k) << (f . k) by A8, A16, WAYBEL_3:def 2;

                end;

                  suppose k <> i;

                  then (f . k) = ( Bottom (J . k)) by A10;

                  then (f . k) is compact by A15, WAYBEL_3: 15;

                  hence (f . k) << (f . k) by WAYBEL_3:def 2;

                end;

              end;

              hence (f . k) << (f . k);

            end;

            ex K be finite Subset of I st for k be Element of I st not k in K holds (f . k) = ( Bottom (J . k))

            proof

              take K = {i};

              let k be Element of I;

              assume not k in K;

              then k <> i by TARSKI:def 1;

              hence thesis by A10;

            end;

            then f << f by A2, A14, WAYBEL_3: 33;

            then f is compact by WAYBEL_3:def 2;

            then f in ( compactbelow x) by A13, WAYBEL_8: 4;

            hence thesis by A6, A11, CARD_3:def 6;

          end;

          ( pi (( compactbelow x),i)) c= ( compactbelow (x . i))

          proof

            let v be object;

            assume v in ( pi (( compactbelow x),i));

            then

            consider f be Function such that

             A17: f in ( compactbelow x) and

             A18: v = (f . i) by CARD_3:def 6;

            f in { y where y be Element of ( product J) : x >= y & y is compact } by A17, WAYBEL_8:def 2;

            then

            consider f1 be Element of ( product J) such that

             A19: f1 = f and

             A20: x >= f1 and

             A21: f1 is compact;

            f1 << f1 by A21, WAYBEL_3:def 2;

            then (f1 . i) << (f1 . i) by A2, WAYBEL_3: 33;

            then

             A22: (f1 . i) is compact by WAYBEL_3:def 2;

            (f1 . i) <= (x . i) by A20, WAYBEL_3: 28;

            hence thesis by A18, A19, A22, WAYBEL_8: 4;

          end;

          

          hence ( sup ( compactbelow (x . i))) = ( sup ( pi (( compactbelow x),i))) by A5, XBOOLE_0:def 10

          .= (( sup ( compactbelow x)) . i) by A2, WAYBEL_3: 32;

        end;

        now

          let i be Element of I;

          (J . i) is satisfying_axiom_K by A1;

          then (x . i) = ( sup ( compactbelow (x . i))) by WAYBEL_8:def 3;

          hence (( sup ( compactbelow x)) . i) <= (x . i) by A4;

        end;

        then

         A23: ( sup ( compactbelow x)) <= x by WAYBEL_3: 28;

        now

          let i be Element of I;

          (J . i) is satisfying_axiom_K by A1;

          then (x . i) = ( sup ( compactbelow (x . i))) by WAYBEL_8:def 3;

          hence (x . i) <= (( sup ( compactbelow x)) . i) by A4;

        end;

        then x <= ( sup ( compactbelow x)) by WAYBEL_3: 28;

        hence x = ( sup ( compactbelow x)) by A3, A23, YELLOW_0:def 3;

      end;

      then

       A24: ( product J) is satisfying_axiom_K by WAYBEL_8:def 3;

      

       A25: for x be Element of L holds ( compactbelow x) is non empty directed

      proof

        let x be Element of L;

        now

          let c,d be Element of L;

          assume that

           A26: c in ( compactbelow x) and

           A27: d in ( compactbelow x);

          d is compact by A27, WAYBEL_8: 4;

          then d <= (c "\/" d) & d << d by WAYBEL_3:def 2, YELLOW_0: 22;

          then

           A28: d << (c "\/" d) by WAYBEL_3: 2;

          c is compact by A26, WAYBEL_8: 4;

          then c <= (c "\/" d) & c << c by WAYBEL_3:def 2, YELLOW_0: 22;

          then c << (c "\/" d) by WAYBEL_3: 2;

          then (c "\/" d) << (c "\/" d) by A28, WAYBEL_3: 3;

          then

           A29: (c "\/" d) is compact by WAYBEL_3:def 2;

          take e = (c "\/" d);

          c <= x & d <= x by A26, A27, WAYBEL_8: 4;

          then (c "\/" d) <= x by YELLOW_0: 22;

          hence e in ( compactbelow x) by A29, WAYBEL_8: 4;

          thus c <= e & d <= e by YELLOW_0: 22;

        end;

        hence thesis by WAYBEL_0:def 1;

      end;

      L is up-complete by A2, WAYBEL_3: 31;

      hence thesis by A25, A24, WAYBEL_8:def 4;

    end;

    

     Lm1: for L be lower-bounded LATTICE holds L is algebraic implies ex X be non empty set, S be full SubRelStr of ( BoolePoset X) st S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic

    proof

      let L be lower-bounded LATTICE;

      assume

       A1: L is algebraic;

      then

      reconsider L9 = L as algebraic lower-bounded LATTICE;

      take X = the carrier of ( CompactSublatt L);

      consider g be Function of L, ( BoolePoset the carrier of ( CompactSublatt L)) such that

       A2: g is infs-preserving and

       A3: g is directed-sups-preserving and

       A4: g is one-to-one and

       A5: for x be Element of L holds (g . x) = ( compactbelow x) by A1, Th24;

      reconsider S = ( Image g) as non empty full SubRelStr of ( BoolePoset X);

      take S;

      

       A6: L9 is complete;

      hence S is infs-inheriting by A2, YELLOW_2: 33;

      

       A7: ( rng g) = the carrier of S by YELLOW_0:def 15;

      ( dom g) = the carrier of L by FUNCT_2:def 1;

      then

      reconsider g1 = g as Function of L, S by A7, FUNCT_2: 1;

      now

        let x,y be Element of L;

        thus x <= y implies (g1 . x) <= (g1 . y)

        proof

          assume x <= y;

          then ( compactbelow x) c= ( compactbelow y) by Th1;

          then (g . x) c= ( compactbelow y) by A5;

          then (g . x) c= (g . y) by A5;

          then (g . x) <= (g . y) by YELLOW_1: 2;

          hence thesis by YELLOW_0: 60;

        end;

        thus (g1 . x) <= (g1 . y) implies x <= y

        proof

          assume (g1 . x) <= (g1 . y);

          then (g . x) <= (g . y) by YELLOW_0: 59;

          then (g . x) c= (g . y) by YELLOW_1: 2;

          then (g . x) c= ( compactbelow y) by A5;

          then

           A8: ( compactbelow x) c= ( compactbelow y) by A5;

           ex_sup_of (( compactbelow x),L) & ex_sup_of (( compactbelow y),L) by A6, YELLOW_0: 17;

          then ( sup ( compactbelow x)) <= ( sup ( compactbelow y)) by A8, YELLOW_0: 34;

          then x <= ( sup ( compactbelow y)) by A1, WAYBEL_8:def 3;

          hence thesis by A1, WAYBEL_8:def 3;

        end;

      end;

      then

       A9: g1 is isomorphic by A4, A7, WAYBEL_0: 66;

      then

      reconsider f1 = (g1 " ) as Function of S, L by WAYBEL_0: 67;

      

       A10: f1 is isomorphic by A9, WAYBEL_0: 68;

      now

        let Y be directed Subset of S;

        assume that

         A11: Y <> {} and ex_sup_of (Y,( BoolePoset X));

        now

          let X2 be finite Subset of (f1 .: Y);

          

           A12: (g1 " (g1 .: X2)) c= X2 by A4, FUNCT_1: 82;

          now

            let v be object;

            assume v in (g1 .: X2);

            then ex u be object st u in ( dom g1) & u in X2 & v = (g1 . u) by FUNCT_1:def 6;

            then v in (g1 .: (f1 .: Y)) by FUNCT_1:def 6;

            then v in (g1 .: (g1 " Y)) by A4, FUNCT_1: 85;

            hence v in Y by A7, FUNCT_1: 77;

          end;

          then

          reconsider Y1 = (g1 .: X2) as finite Subset of Y by TARSKI:def 3;

          consider y1 be Element of S such that

           A13: y1 in Y and

           A14: y1 is_>=_than Y1 by A11, WAYBEL_0: 1;

          take f1y1 = (f1 . y1);

          y1 in the carrier of S;

          then y1 in ( dom f1) by FUNCT_2:def 1;

          hence f1y1 in (f1 .: Y) by A13, FUNCT_1:def 6;

          X2 c= the carrier of L by XBOOLE_1: 1;

          then X2 c= ( dom g1) by FUNCT_2:def 1;

          then

           A15: X2 c= (g1 " (g1 .: X2)) by FUNCT_1: 76;

          (f1 .: Y1) = (g1 " (g1 .: X2)) by A4, FUNCT_1: 85

          .= X2 by A15, A12, XBOOLE_0:def 10;

          hence f1y1 is_>=_than X2 by A10, A14, Th19;

        end;

        then

        reconsider X1 = (f1 .: Y) as non empty directed Subset of L by WAYBEL_0: 1;

        ( sup X1) in the carrier of L;

        then ( sup X1) in ( dom g) by FUNCT_2:def 1;

        then

         A16: (g . ( sup X1)) in ( rng g) by FUNCT_1:def 3;

         ex_sup_of (X1,L) & g preserves_sup_of X1 by A6, A3, WAYBEL_0:def 37, YELLOW_0: 17;

        then

         A17: ( sup (g .: X1)) in ( rng g) by A16, WAYBEL_0:def 31;

        (g .: X1) = (g .: (g1 " Y)) by A4, FUNCT_1: 85

        .= Y by A7, FUNCT_1: 77;

        hence ( "\/" (Y,( BoolePoset X))) in the carrier of S by A17, YELLOW_0:def 15;

      end;

      hence S is directed-sups-inheriting by WAYBEL_0:def 4;

      thus thesis by A9, WAYBEL_1:def 8;

    end;

    theorem :: WAYBEL13:26

    

     Th26: for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr of L2 holds (L1,L2) are_isomorphic

    proof

      let L1,L2 be non empty RelStr;

      assume

       A1: the RelStr of L1 = the RelStr of L2;

      ex f be Function of L1, L2 st f is isomorphic

      proof

        reconsider f = ( id the carrier of L1) as Function of L1, L2 by A1;

        take f;

        now

          let z be object;

          assume

           A2: z in the carrier of L2;

          take v = z;

          thus v in the carrier of L1 by A1, A2;

          thus z = (f . v) by A1, A2, FUNCT_1: 18;

        end;

        then

         A3: ( rng f) = the carrier of L2 by FUNCT_2: 10;

        for x,y be Element of L1 holds x <= y iff (f . x) <= (f . y) by A1, YELLOW_0: 1;

        hence thesis by A3, WAYBEL_0: 66;

      end;

      hence thesis by WAYBEL_1:def 8;

    end;

    

     Lm2: for L be LATTICE holds (ex X be non empty set, S be full SubRelStr of ( BoolePoset X) st (S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic )) implies ex X be non empty set, c be closure Function of ( BoolePoset X), ( BoolePoset X) st c is directed-sups-preserving & (L,( Image c)) are_isomorphic

    proof

      let L be LATTICE;

      given X be non empty set, S be full SubRelStr of ( BoolePoset X) such that

       A1: S is infs-inheriting and

       A2: S is directed-sups-inheriting and

       A3: (L,S) are_isomorphic ;

      reconsider S9 = S as closure System of ( BoolePoset X) by A1;

      take X;

      reconsider c = ( closure_op S9) as closure Function of ( BoolePoset X), ( BoolePoset X);

      take c;

      thus c is directed-sups-preserving by A2;

      ( Image c) = the RelStr of S by WAYBEL10: 18;

      then (S,( Image c)) are_isomorphic by Th26;

      hence thesis by A3, WAYBEL_1: 7;

    end;

    

     Lm3: for L be LATTICE holds (ex X be set, S be full SubRelStr of ( BoolePoset X) st (S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic )) implies ex X be set, c be closure Function of ( BoolePoset X), ( BoolePoset X) st c is directed-sups-preserving & (L,( Image c)) are_isomorphic

    proof

      let L be LATTICE;

      given X be set, S be full SubRelStr of ( BoolePoset X) such that

       A1: S is infs-inheriting and

       A2: S is directed-sups-inheriting and

       A3: (L,S) are_isomorphic ;

      reconsider S9 = S as closure System of ( BoolePoset X) by A1;

      take X;

      reconsider c = ( closure_op S9) as closure Function of ( BoolePoset X), ( BoolePoset X);

      take c;

      thus c is directed-sups-preserving by A2;

      ( Image c) = the RelStr of S by WAYBEL10: 18;

      then (S,( Image c)) are_isomorphic by Th26;

      hence thesis by A3, WAYBEL_1: 7;

    end;

    

     Lm4: for L1,L2 be up-complete non empty Poset holds for f be Function of L1, L2 st f is isomorphic holds for x,y be Element of L1 holds x << y implies (f . x) << (f . y)

    proof

      let L1,L2 be up-complete non empty Poset;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      then

      reconsider g = (f " ) as Function of L2, L1 by WAYBEL_0: 67;

      let x,y be Element of L1;

      

       A2: g is isomorphic by A1, WAYBEL_0: 68;

      assume

       A3: x << y;

      now

        let X be non empty directed Subset of L2;

        y in the carrier of L1;

        then

         A4: y in ( dom f) by FUNCT_2:def 1;

        X c= the carrier of L2;

        then

         A5: X c= ( rng f) by A1, WAYBEL_0: 66;

        now

          let Y1 be finite Subset of (g .: X);

          

           A6: (f " (f .: Y1)) c= Y1 by A1, FUNCT_1: 82;

          now

            let v be object;

            assume v in (f .: Y1);

            then ex u be object st u in ( dom f) & u in Y1 & v = (f . u) by FUNCT_1:def 6;

            then v in (f .: (g .: X)) by FUNCT_1:def 6;

            then v in (f .: (f " X)) by A1, FUNCT_1: 85;

            hence v in X by A5, FUNCT_1: 77;

          end;

          then

          reconsider X1 = (f .: Y1) as finite Subset of X by TARSKI:def 3;

          consider y1 be Element of L2 such that

           A7: y1 in X and

           A8: y1 is_>=_than X1 by WAYBEL_0: 1;

          take gy1 = (g . y1);

          y1 in the carrier of L2;

          then y1 in ( dom g) by FUNCT_2:def 1;

          hence gy1 in (g .: X) by A7, FUNCT_1:def 6;

          Y1 c= the carrier of L1 by XBOOLE_1: 1;

          then Y1 c= ( dom f) by FUNCT_2:def 1;

          then

           A9: Y1 c= (f " (f .: Y1)) by FUNCT_1: 76;

          (g .: X1) = (f " (f .: Y1)) by A1, FUNCT_1: 85

          .= Y1 by A9, A6, XBOOLE_0:def 10;

          hence gy1 is_>=_than Y1 by A2, A8, Th19;

        end;

        then

        reconsider Y = (g .: X) as non empty directed Subset of L1 by WAYBEL_0: 1;

        

         A10: ex_sup_of (X,L2) & g preserves_sup_of X by A2, WAYBEL_0: 75, WAYBEL_0:def 33;

        assume (f . y) <= ( sup X);

        then (g . (f . y)) <= (g . ( sup X)) by A2, WAYBEL_0: 66;

        then y <= (g . ( sup X)) by A1, A4, FUNCT_1: 34;

        then y <= ( sup Y) by A10, WAYBEL_0:def 31;

        then

        consider c be Element of L1 such that

         A11: c in Y and

         A12: x <= c by A3, WAYBEL_3:def 1;

        take fc = (f . c);

        c in the carrier of L1;

        then c in ( dom f) by FUNCT_2:def 1;

        then (f . c) in (f .: Y) by A11, FUNCT_1:def 6;

        then (f . c) in (f .: (f " X)) by A1, FUNCT_1: 85;

        hence fc in X by A5, FUNCT_1: 77;

        thus (f . x) <= fc by A1, A12, WAYBEL_0: 66;

      end;

      hence thesis by WAYBEL_3:def 1;

    end;

    theorem :: WAYBEL13:27

    

     Th27: for L1,L2 be up-complete non empty Poset holds for f be Function of L1, L2 st f is isomorphic holds for x,y be Element of L1 holds x << y iff (f . x) << (f . y)

    proof

      let L1,L2 be up-complete non empty Poset;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      then

      reconsider g = (f " ) as Function of L2, L1 by WAYBEL_0: 67;

      let x,y be Element of L1;

      thus x << y implies (f . x) << (f . y) by A1, Lm4;

      thus (f . x) << (f . y) implies x << y

      proof

        y in the carrier of L1;

        then

         A2: y in ( dom f) by FUNCT_2:def 1;

        x in the carrier of L1;

        then

         A3: x in ( dom f) by FUNCT_2:def 1;

        assume (f . x) << (f . y);

        then (g . (f . x)) << (g . (f . y)) by A1, Lm4, WAYBEL_0: 68;

        then x << (g . (f . y)) by A1, A3, FUNCT_1: 34;

        hence thesis by A1, A2, FUNCT_1: 34;

      end;

    end;

    theorem :: WAYBEL13:28

    

     Th28: for L1,L2 be up-complete non empty Poset holds for f be Function of L1, L2 st f is isomorphic holds for x be Element of L1 holds x is compact iff (f . x) is compact

    proof

      let L1,L2 be up-complete non empty Poset;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      let x be Element of L1;

      thus x is compact implies (f . x) is compact

      proof

        assume x is compact;

        then x << x by WAYBEL_3:def 2;

        then (f . x) << (f . x) by A1, Th27;

        hence thesis by WAYBEL_3:def 2;

      end;

      thus (f . x) is compact implies x is compact

      proof

        assume (f . x) is compact;

        then (f . x) << (f . x) by WAYBEL_3:def 2;

        then x << x by A1, Th27;

        hence thesis by WAYBEL_3:def 2;

      end;

    end;

    theorem :: WAYBEL13:29

    

     Th29: for L1,L2 be up-complete non empty Poset holds for f be Function of L1, L2 st f is isomorphic holds for x be Element of L1 holds (f .: ( compactbelow x)) = ( compactbelow (f . x))

    proof

      let L1,L2 be up-complete non empty Poset;

      let f be Function of L1, L2;

      assume

       A1: f is isomorphic;

      then

      reconsider g = (f " ) as Function of L2, L1 by WAYBEL_0: 67;

      let x be Element of L1;

      

       A2: g is isomorphic by A1, WAYBEL_0: 68;

      

       A3: ( compactbelow (f . x)) c= (f .: ( compactbelow x))

      proof

        let z be object;

        x in the carrier of L1;

        then

         A4: x in ( dom f) by FUNCT_2:def 1;

        assume z in ( compactbelow (f . x));

        then z in { y where y be Element of L2 : (f . x) >= y & y is compact } by WAYBEL_8:def 2;

        then

        consider z1 be Element of L2 such that

         A5: z1 = z and

         A6: (f . x) >= z1 and

         A7: z1 is compact;

        

         A8: (g . z1) is compact by A2, A7, Th28;

        (g . z1) <= (g . (f . x)) by A2, A6, WAYBEL_0: 66;

        then (g . z1) <= x by A1, A4, FUNCT_1: 34;

        then

         A9: (g . z1) in ( compactbelow x) by A8, WAYBEL_8: 4;

        z1 in the carrier of L2;

        then

         A10: z1 in ( rng f) by A1, WAYBEL_0: 66;

        (g . z1) in the carrier of L1;

        then (g . z1) in ( dom f) by FUNCT_2:def 1;

        then (f . (g . z1)) in (f .: ( compactbelow x)) by A9, FUNCT_1:def 6;

        hence thesis by A1, A5, A10, FUNCT_1: 35;

      end;

      (f .: ( compactbelow x)) c= ( compactbelow (f . x))

      proof

        let z be object;

        assume z in (f .: ( compactbelow x));

        then

        consider u be object such that u in ( dom f) and

         A11: u in ( compactbelow x) and

         A12: z = (f . u) by FUNCT_1:def 6;

        u in { y where y be Element of L1 : x >= y & y is compact } by A11, WAYBEL_8:def 2;

        then

        consider u1 be Element of L1 such that

         A13: u1 = u and

         A14: x >= u1 & u1 is compact;

        (f . u1) <= (f . x) & (f . u1) is compact by A1, A14, Th28, WAYBEL_0: 66;

        hence thesis by A12, A13, WAYBEL_8: 4;

      end;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: WAYBEL13:30

    

     Th30: for L1,L2 be non empty Poset st (L1,L2) are_isomorphic & L1 is up-complete holds L2 is up-complete

    proof

      let L1,L2 be non empty Poset;

      assume that

       A1: (L1,L2) are_isomorphic and

       A2: L1 is up-complete;

      consider f be Function of L1, L2 such that

       A3: f is isomorphic by A1, WAYBEL_1:def 8;

      reconsider g = (f " ) as Function of L2, L1 by A3, WAYBEL_0: 67;

      

       A4: g is isomorphic by A3, WAYBEL_0: 68;

      now

        let Y be non empty directed Subset of L2;

        Y c= the carrier of L2;

        then

         A5: Y c= ( rng f) by A3, WAYBEL_0: 66;

        now

          let X1 be finite Subset of (g .: Y);

          

           A6: (f " (f .: X1)) c= X1 by A3, FUNCT_1: 82;

          now

            let v be object;

            assume v in (f .: X1);

            then ex u be object st u in ( dom f) & u in X1 & v = (f . u) by FUNCT_1:def 6;

            then v in (f .: (g .: Y)) by FUNCT_1:def 6;

            then v in (f .: (f " Y)) by A3, FUNCT_1: 85;

            hence v in Y by A5, FUNCT_1: 77;

          end;

          then

          reconsider Y1 = (f .: X1) as finite Subset of Y by TARSKI:def 3;

          consider y1 be Element of L2 such that

           A7: y1 in Y and

           A8: y1 is_>=_than Y1 by WAYBEL_0: 1;

          take gy1 = (g . y1);

          y1 in the carrier of L2;

          then y1 in ( dom g) by FUNCT_2:def 1;

          hence gy1 in (g .: Y) by A7, FUNCT_1:def 6;

          X1 c= the carrier of L1 by XBOOLE_1: 1;

          then X1 c= ( dom f) by FUNCT_2:def 1;

          then

           A9: X1 c= (f " (f .: X1)) by FUNCT_1: 76;

          (g .: Y1) = (f " (f .: X1)) by A3, FUNCT_1: 85

          .= X1 by A9, A6, XBOOLE_0:def 10;

          hence gy1 is_>=_than X1 by A4, A8, Th19;

        end;

        then

        reconsider X = (g .: Y) as non empty directed Subset of L1 by WAYBEL_0: 1;

         ex_sup_of (X,L1) by A2, WAYBEL_0: 75;

        then

        consider x be Element of L1 such that

         A10: X is_<=_than x and

         A11: for b be Element of L1 st X is_<=_than b holds x <= b by YELLOW_0: 15;

         A12:

        now

          let y be Element of L2;

          assume Y is_<=_than y;

          then X is_<=_than (g . y) by A4, Th19;

          then x <= (g . y) by A11;

          then

           A13: (f . x) <= (f . (g . y)) by A3, WAYBEL_0: 66;

          y in the carrier of L2;

          then y in ( dom g) by FUNCT_2:def 1;

          then y in ( rng f) by A3, FUNCT_1: 33;

          hence (f . x) <= y by A3, A13, FUNCT_1: 35;

        end;

        (f .: X) = (f .: (f " Y)) by A3, FUNCT_1: 85

        .= Y by A5, FUNCT_1: 77;

        then Y is_<=_than (f . x) by A3, A10, Th19;

        hence ex_sup_of (Y,L2) by A12, YELLOW_0: 15;

      end;

      hence thesis by WAYBEL_0: 75;

    end;

    theorem :: WAYBEL13:31

    

     Th31: for L1,L2 be non empty Poset st (L1,L2) are_isomorphic & L1 is complete satisfying_axiom_K holds L2 is satisfying_axiom_K

    proof

      let L1,L2 be non empty Poset;

      assume that

       A1: (L1,L2) are_isomorphic and

       A2: L1 is complete satisfying_axiom_K;

      consider f be Function of L1, L2 such that

       A3: f is isomorphic by A1, WAYBEL_1:def 8;

      reconsider g = (f " ) as Function of L2, L1 by A3, WAYBEL_0: 67;

      now

        let x be Element of L2;

        

         A4: f preserves_sup_of ( compactbelow (g . x)) & ex_sup_of (( compactbelow (g . x)),L1) by A2, A3, WAYBEL_0:def 33, YELLOW_0: 17;

        

         A5: L2 is up-complete non empty Poset by A1, A2, Th30;

        x in the carrier of L2;

        then x in ( dom g) by FUNCT_2:def 1;

        then

         A6: x in ( rng f) by A3, FUNCT_1: 33;

        

        hence x = (f . (g . x)) by A3, FUNCT_1: 35

        .= (f . ( sup ( compactbelow (g . x)))) by A2, WAYBEL_8:def 3

        .= ( sup (f .: ( compactbelow (g . x)))) by A4, WAYBEL_0:def 31

        .= ( sup ( compactbelow (f . (g . x)))) by A2, A3, A5, Th29

        .= ( sup ( compactbelow x)) by A3, A6, FUNCT_1: 35;

      end;

      hence thesis by WAYBEL_8:def 3;

    end;

    theorem :: WAYBEL13:32

    

     Th32: for L1,L2 be sup-Semilattice st (L1,L2) are_isomorphic & L1 is lower-bounded algebraic holds L2 is algebraic

    proof

      let L1,L2 be sup-Semilattice;

      assume that

       A1: (L1,L2) are_isomorphic and

       A2: L1 is lower-bounded algebraic;

      consider f be Function of L1, L2 such that

       A3: f is isomorphic by A1, WAYBEL_1:def 8;

      reconsider g = (f " ) as Function of L2, L1 by A3, WAYBEL_0: 67;

      

       A4: g is isomorphic by A3, WAYBEL_0: 68;

       A5:

      now

        let y be Element of L2;

        y in the carrier of L2;

        then y in ( dom g) by FUNCT_2:def 1;

        then

         A6: y in ( rng f) by A3, FUNCT_1: 33;

        

         A7: L2 is up-complete non empty Poset by A1, A2, Th30;

        

         A8: ( compactbelow (g . y)) is non empty directed by A2, WAYBEL_8:def 4;

        now

          let Y be finite Subset of ( compactbelow (f . (g . y)));

          Y c= the carrier of L2 by XBOOLE_1: 1;

          then

           A9: Y c= ( rng f) by A3, WAYBEL_0: 66;

          now

            let z be object;

            assume z in (g .: Y);

            then

            consider v be object such that

             A10: v in ( dom g) and

             A11: v in Y and

             A12: z = (g . v) by FUNCT_1:def 6;

            reconsider v as Element of L2 by A10;

            v in ( compactbelow (f . (g . y))) by A11;

            then v in ( compactbelow y) by A3, A6, FUNCT_1: 35;

            then v <= y by WAYBEL_8: 4;

            then

             A13: (g . v) <= (g . y) by A4, WAYBEL_0: 66;

            v is compact by A11, WAYBEL_8: 4;

            then (g . v) is compact by A2, A4, A7, Th28;

            hence z in ( compactbelow (g . y)) by A12, A13, WAYBEL_8: 4;

          end;

          then

          reconsider X = (g .: Y) as finite Subset of ( compactbelow (g . y)) by TARSKI:def 3;

          consider x be Element of L1 such that

           A14: x in ( compactbelow (g . y)) and

           A15: x is_>=_than X by A8, WAYBEL_0: 1;

          take fx = (f . x);

          x <= (g . y) by A14, WAYBEL_8: 4;

          then

           A16: (f . x) <= (f . (g . y)) by A3, WAYBEL_0: 66;

          x is compact by A14, WAYBEL_8: 4;

          then (f . x) is compact by A2, A3, A7, Th28;

          hence fx in ( compactbelow (f . (g . y))) by A16, WAYBEL_8: 4;

          (f .: X) = (f .: (f " Y)) by A3, FUNCT_1: 85

          .= Y by A9, FUNCT_1: 77;

          hence fx is_>=_than Y by A3, A15, Th19;

        end;

        then ( compactbelow (f . (g . y))) is non empty directed by WAYBEL_0: 1;

        hence ( compactbelow y) is non empty directed by A3, A6, FUNCT_1: 35;

      end;

      L2 is up-complete & L2 is satisfying_axiom_K by A1, A2, Th30, Th31;

      hence thesis by A5, WAYBEL_8:def 4;

    end;

    

     Lm5: for L be LATTICE holds (ex X be set, c be closure Function of ( BoolePoset X), ( BoolePoset X) st c is directed-sups-preserving & (L,( Image c)) are_isomorphic ) implies L is algebraic

    proof

      let L be LATTICE;

      given X be set, c be closure Function of ( BoolePoset X), ( BoolePoset X) such that

       A1: c is directed-sups-preserving and

       A2: (L,( Image c)) are_isomorphic ;

      ( Image c) is complete LATTICE & ( Image c) is algebraic LATTICE by A1, WAYBEL_8: 24, YELLOW_2: 35;

      hence thesis by A2, Th32, WAYBEL_1: 6;

    end;

    theorem :: WAYBEL13:33

    for L be continuous lower-bounded sup-Semilattice holds ( SupMap L) is infs-preserving sups-preserving by WAYBEL_1: 12, WAYBEL_1: 57, WAYBEL_5: 3;

    theorem :: WAYBEL13:34

    for L be lower-bounded LATTICE holds (L is algebraic implies ex X be non empty set, S be full SubRelStr of ( BoolePoset X) st S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic ) & ((ex X be set, S be full SubRelStr of ( BoolePoset X) st S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic ) implies L is algebraic)

    proof

      let L be lower-bounded LATTICE;

      thus L is algebraic implies ex X be non empty set, S be full SubRelStr of ( BoolePoset X) st S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic by Lm1;

      thus (ex X be set, S be full SubRelStr of ( BoolePoset X) st (S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic )) implies L is algebraic

      proof

        assume ex X be set, S be full SubRelStr of ( BoolePoset X) st S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic ;

        then ex X be set, c be closure Function of ( BoolePoset X), ( BoolePoset X) st c is directed-sups-preserving & (L,( Image c)) are_isomorphic by Lm3;

        hence thesis by Lm5;

      end;

    end;

    theorem :: WAYBEL13:35

    for L be lower-bounded LATTICE holds (L is algebraic implies ex X be non empty set, c be closure Function of ( BoolePoset X), ( BoolePoset X) st c is directed-sups-preserving & (L,( Image c)) are_isomorphic ) & ((ex X be set, c be closure Function of ( BoolePoset X), ( BoolePoset X) st c is directed-sups-preserving & (L,( Image c)) are_isomorphic ) implies L is algebraic)

    proof

      let L be lower-bounded LATTICE;

      hereby

        assume L is algebraic;

        then ex X be non empty set, S be full SubRelStr of ( BoolePoset X) st S is infs-inheriting & S is directed-sups-inheriting & (L,S) are_isomorphic by Lm1;

        hence ex X be non empty set, c be closure Function of ( BoolePoset X), ( BoolePoset X) st c is directed-sups-preserving & (L,( Image c)) are_isomorphic by Lm2;

      end;

      thus thesis by Lm5;

    end;