waybel_0.miz



    begin

    definition

      let L be RelStr;

      let X be Subset of L;

      :: WAYBEL_0:def1

      attr X is directed means

      : Def1: for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x <= z & y <= z;

      :: WAYBEL_0:def2

      attr X is filtered means

      : Def2: for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & z <= x & z <= y;

    end

    theorem :: WAYBEL_0:1

    

     Th1: for L be non empty transitive RelStr, X be Subset of L holds X is non empty directed iff for Y be finite Subset of X holds ex x be Element of L st x in X & x is_>=_than Y

    proof

      let L be non empty transitive RelStr, X be Subset of L;

      hereby

        assume X is non empty;

        then

        reconsider X9 = X as non empty set;

        assume

         A1: X is directed;

        let Y be finite Subset of X;

        defpred P[ set] means ex x be Element of L st x in X & x is_>=_than $1;

        

         A2: Y is finite;

        set x = the Element of X9;

        x in X;

        then

        reconsider x as Element of L;

        x is_>=_than {} ;

        then

         A3: P[ {} ];

         A4:

        now

          let x,B be set;

          assume that

           A5: x in Y and B c= Y;

          assume P[B];

          then

          consider y be Element of L such that

           A6: y in X and

           A7: y is_>=_than B;

          x in X by A5;

          then

          reconsider x9 = x as Element of L;

          consider z be Element of L such that

           A8: z in X and

           A9: x9 <= z and

           A10: y <= z by A1, A5, A6;

          thus P[(B \/ {x})]

          proof

            take z;

            thus z in X by A8;

            let a be Element of L;

            reconsider a9 = a as Element of L;

            assume a in (B \/ {x});

            then a9 in B or a9 in {x} by XBOOLE_0:def 3;

            then y >= a9 or a9 = x by A7, TARSKI:def 1;

            hence thesis by A9, A10, ORDERS_2: 3;

          end;

        end;

        thus P[Y] from FINSET_1:sch 2( A2, A3, A4);

      end;

      assume

       A11: for Y be finite Subset of X holds ex x be Element of L st x in X & x is_>=_than Y;

       {} c= X;

      then ex x be Element of L st x in X & x is_>=_than {} by A11;

      hence X is non empty;

      let x,y be Element of L;

      assume that

       A12: x in X and

       A13: y in X;

       {x, y} c= X by A12, A13, ZFMISC_1: 32;

      then

      consider z be Element of L such that

       A14: z in X and

       A15: z is_>=_than {x, y} by A11;

      take z;

      

       A16: x in {x, y} by TARSKI:def 2;

      y in {x, y} by TARSKI:def 2;

      hence thesis by A14, A15, A16;

    end;

    theorem :: WAYBEL_0:2

    

     Th2: for L be non empty transitive RelStr, X be Subset of L holds X is non empty filtered iff for Y be finite Subset of X holds ex x be Element of L st x in X & x is_<=_than Y

    proof

      let L be non empty transitive RelStr, X be Subset of L;

      hereby

        assume X is non empty;

        then

        reconsider X9 = X as non empty set;

        assume

         A1: X is filtered;

        let Y be finite Subset of X;

        defpred P[ set] means ex x be Element of L st x in X & x is_<=_than $1;

        

         A2: Y is finite;

        set x = the Element of X9;

        x in X;

        then

        reconsider x as Element of L;

        x is_<=_than {} ;

        then

         A3: P[ {} ];

         A4:

        now

          let x,B be set;

          assume that

           A5: x in Y and B c= Y;

          assume P[B];

          then

          consider y be Element of L such that

           A6: y in X and

           A7: y is_<=_than B;

          x in X by A5;

          then

          reconsider x9 = x as Element of L;

          consider z be Element of L such that

           A8: z in X and

           A9: x9 >= z and

           A10: y >= z by A1, A5, A6;

          thus P[(B \/ {x})]

          proof

            take z;

            thus z in X by A8;

            let a be Element of L;

            reconsider a9 = a as Element of L;

            assume a in (B \/ {x});

            then a9 in B or a9 in {x} by XBOOLE_0:def 3;

            then y <= a9 or a9 = x by A7, TARSKI:def 1;

            hence thesis by A9, A10, ORDERS_2: 3;

          end;

        end;

        thus P[Y] from FINSET_1:sch 2( A2, A3, A4);

      end;

      assume

       A11: for Y be finite Subset of X holds ex x be Element of L st x in X & x is_<=_than Y;

       {} c= X;

      then ex x be Element of L st x in X & x is_<=_than {} by A11;

      hence X is non empty;

      let x,y be Element of L;

      assume that

       A12: x in X and

       A13: y in X;

       {x, y} c= X by A12, A13, ZFMISC_1: 32;

      then

      consider z be Element of L such that

       A14: z in X and

       A15: z is_<=_than {x, y} by A11;

      take z;

      

       A16: x in {x, y} by TARSKI:def 2;

      y in {x, y} by TARSKI:def 2;

      hence thesis by A14, A15, A16;

    end;

    registration

      let L be RelStr;

      cluster empty -> directed filtered for Subset of L;

      coherence ;

    end

    registration

      let L be RelStr;

      cluster directed filtered for Subset of L;

      existence

      proof

        take ( {} L);

        thus thesis;

      end;

    end

    theorem :: WAYBEL_0:3

    

     Th3: for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 holds for X1 be Subset of L1, X2 be Subset of L2 st X1 = X2 & X1 is directed holds X2 is directed

    proof

      let L1,L2 be RelStr such that

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

      let X1 be Subset of L1, X2 be Subset of L2 such that

       A2: X1 = X2;

      assume

       A3: for x,y be Element of L1 st x in X1 & y in X1 holds ex z be Element of L1 st z in X1 & x <= z & y <= z;

      let x,y be Element of L2;

      reconsider x9 = x, y9 = y as Element of L1 by A1;

      assume that

       A4: x in X2 and

       A5: y in X2;

      consider z9 be Element of L1 such that

       A6: z9 in X1 and

       A7: x9 <= z9 and

       A8: y9 <= z9 by A2, A3, A4, A5;

      reconsider z = z9 as Element of L2 by A1;

      take z;

      thus thesis by A1, A2, A6, A7, A8, YELLOW_0: 1;

    end;

    theorem :: WAYBEL_0:4

    for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 holds for X1 be Subset of L1, X2 be Subset of L2 st X1 = X2 & X1 is filtered holds X2 is filtered

    proof

      let L1,L2 be RelStr such that

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

      let X1 be Subset of L1, X2 be Subset of L2 such that

       A2: X1 = X2;

      assume

       A3: for x,y be Element of L1 st x in X1 & y in X1 holds ex z be Element of L1 st z in X1 & x >= z & y >= z;

      let x,y be Element of L2;

      reconsider x9 = x, y9 = y as Element of L1 by A1;

      assume that

       A4: x in X2 and

       A5: y in X2;

      consider z9 be Element of L1 such that

       A6: z9 in X1 and

       A7: x9 >= z9 and

       A8: y9 >= z9 by A2, A3, A4, A5;

      reconsider z = z9 as Element of L2 by A1;

      take z;

      thus thesis by A1, A2, A6, A7, A8, YELLOW_0: 1;

    end;

    theorem :: WAYBEL_0:5

    

     Th5: for L be non empty reflexive RelStr, x be Element of L holds {x} is directed filtered

    proof

      let L be non empty reflexive RelStr;

      let x be Element of L;

      set X = {x};

      hereby

        let z,y be Element of L;

        assume that

         A1: z in X and

         A2: y in X;

        take x;

        thus x in X & z <= x & y <= x by A1, A2, TARSKI:def 1;

      end;

      hereby

        let z,y be Element of L;

        assume that

         A3: z in X and

         A4: y in X;

        take x;

        thus x in X & x <= z & x <= y by A3, A4, TARSKI:def 1;

      end;

    end;

    registration

      let L be non empty reflexive RelStr;

      cluster directed filtered non empty finite for Subset of L;

      existence

      proof

        set x = the Element of L;

        take {x};

        thus thesis by Th5;

      end;

    end

    registration

      let L be with_suprema RelStr;

      cluster ( [#] L) -> directed;

      coherence

      proof

        set X = ( [#] L);

        let x,y be Element of L;

        assume that x in X and y in X;

        ex z be Element of L st x <= z & y <= z & for z9 be Element of L st x <= z9 & y <= z9 holds z <= z9 by LATTICE3:def 10;

        hence thesis;

      end;

    end

    registration

      let L be upper-bounded non empty RelStr;

      cluster ( [#] L) -> directed;

      coherence

      proof

        set X = ( [#] L);

        let x,y be Element of L;

        assume that x in X and y in X;

        consider z be Element of L such that

         A1: z is_>=_than X by YELLOW_0:def 5;

        take z;

        thus thesis by A1;

      end;

    end

    registration

      let L be with_infima RelStr;

      cluster ( [#] L) -> filtered;

      coherence

      proof

        set X = ( [#] L);

        let x,y be Element of L such that x in X and y in X;

        ex z be Element of L st z <= x & z <= y & for z9 be Element of L st z9 <= x & z9 <= y holds z9 <= z by LATTICE3:def 11;

        hence thesis;

      end;

    end

    registration

      let L be lower-bounded non empty RelStr;

      cluster ( [#] L) -> filtered;

      coherence

      proof

        set X = ( [#] L);

        let x,y be Element of L;

        assume that x in X and y in X;

        consider z be Element of L such that

         A1: z is_<=_than X by YELLOW_0:def 4;

        take z;

        thus thesis by A1;

      end;

    end

    definition

      let L be non empty RelStr;

      let S be SubRelStr of L;

      :: WAYBEL_0:def3

      attr S is filtered-infs-inheriting means

      : Def3: for X be filtered Subset of S st X <> {} & ex_inf_of (X,L) holds ( "/\" (X,L)) in the carrier of S;

      :: WAYBEL_0:def4

      attr S is directed-sups-inheriting means

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

    end

    registration

      let L be non empty RelStr;

      cluster infs-inheriting -> filtered-infs-inheriting for SubRelStr of L;

      coherence ;

      cluster sups-inheriting -> directed-sups-inheriting for SubRelStr of L;

      coherence ;

    end

    registration

      let L be non empty RelStr;

      cluster infs-inheriting sups-inheriting non empty full strict for SubRelStr of L;

      existence

      proof

        set S = the infs-inheriting sups-inheriting non empty full strict SubRelStr of L;

        take S;

        thus thesis;

      end;

    end

    theorem :: WAYBEL_0:6

    for L be non empty transitive RelStr holds for S be filtered-infs-inheriting non empty full SubRelStr of L holds for X be filtered Subset of S st X <> {} & ex_inf_of (X,L) holds ex_inf_of (X,S) & ( "/\" (X,S)) = ( "/\" (X,L))

    proof

      let L be non empty transitive RelStr;

      let S be filtered-infs-inheriting non empty full SubRelStr of L;

      let X be filtered Subset of S;

      assume that

       A1: X <> {} and

       A2: ex_inf_of (X,L);

      ( "/\" (X,L)) in the carrier of S by A1, A2, Def3;

      hence thesis by A2, YELLOW_0: 63;

    end;

    theorem :: WAYBEL_0:7

    for L be non empty transitive RelStr holds for S be directed-sups-inheriting non empty full SubRelStr of L holds for X be directed Subset of S st X <> {} & ex_sup_of (X,L) holds ex_sup_of (X,S) & ( "\/" (X,S)) = ( "\/" (X,L))

    proof

      let L be non empty transitive RelStr;

      let S be directed-sups-inheriting non empty full SubRelStr of L;

      let X be directed Subset of S;

      assume that

       A1: X <> {} and

       A2: ex_sup_of (X,L);

      ( "\/" (X,L)) in the carrier of S by A1, A2, Def4;

      hence thesis by A2, YELLOW_0: 64;

    end;

    begin

    definition

      let L1,L2 be RelStr;

      let f be Function of L1, L2;

      :: WAYBEL_0:def5

      attr f is antitone means for x,y be Element of L1 st x <= y holds for a,b be Element of L2 st a = (f . x) & b = (f . y) holds a >= b;

    end

    definition

      let L be 1-sorted;

      struct ( RelStr) NetStr over L (# the carrier -> set,

the InternalRel -> Relation of the carrier,

the mapping -> Function of the carrier, the carrier of L #)

       attr strict strict;

    end

    registration

      let L be 1-sorted;

      let X be non empty set;

      let O be Relation of X;

      let F be Function of X, the carrier of L;

      cluster NetStr (# X, O, F #) -> non empty;

      coherence ;

    end

    definition

      let N be RelStr;

      :: WAYBEL_0:def6

      attr N is directed means

      : Def6: ( [#] N) is directed;

    end

    registration

      let L be 1-sorted;

      cluster non empty reflexive transitive antisymmetric directed for strict NetStr over L;

      existence

      proof

        set X = the with_suprema Poset;

        set M = the Function of the carrier of X, the carrier of L;

        take N = NetStr (# the carrier of X, the InternalRel of X, M #);

        thus N is non empty;

        

         A1: the InternalRel of N is_reflexive_in the carrier of N by ORDERS_2:def 2;

        

         A2: the InternalRel of N is_transitive_in the carrier of N by ORDERS_2:def 3;

        the InternalRel of N is_antisymmetric_in the carrier of N by ORDERS_2:def 4;

        hence N is reflexive transitive antisymmetric by A1, A2, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

        

         A3: the RelStr of N = the RelStr of X;

        ( [#] X) = ( [#] N);

        hence ( [#] N) is directed by A3, Th3;

      end;

    end

    definition

      let L be 1-sorted;

      mode prenet of L is directed non empty NetStr over L;

    end

    definition

      let L be 1-sorted;

      mode net of L is transitive prenet of L;

    end

    definition

      let L be non empty 1-sorted;

      let N be non empty NetStr over L;

      :: WAYBEL_0:def7

      func netmap (N,L) -> Function of N, L equals the mapping of N;

      coherence ;

      let i be Element of N;

      :: WAYBEL_0:def8

      func N . i -> Element of L equals (the mapping of N . i);

      correctness ;

    end

    definition

      let L be non empty RelStr;

      let N be non empty NetStr over L;

      :: WAYBEL_0:def9

      attr N is monotone means ( netmap (N,L)) is monotone;

      :: WAYBEL_0:def10

      attr N is antitone means ( netmap (N,L)) is antitone;

    end

    definition

      let L be non empty 1-sorted;

      let N be non empty NetStr over L;

      let X be set;

      :: WAYBEL_0:def11

      pred N is_eventually_in X means ex i be Element of N st for j be Element of N st i <= j holds (N . j) in X;

      :: WAYBEL_0:def12

      pred N is_often_in X means for i be Element of N holds ex j be Element of N st i <= j & (N . j) in X;

    end

    theorem :: WAYBEL_0:8

    for L be non empty 1-sorted, N be non empty NetStr over L holds for X,Y be set st X c= Y holds (N is_eventually_in X implies N is_eventually_in Y) & (N is_often_in X implies N is_often_in Y)

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L;

      let X,Y be set such that

       A1: X c= Y;

      hereby

        assume N is_eventually_in X;

        then

        consider i be Element of N such that

         A2: for j be Element of N st i <= j holds (N . j) in X;

        thus N is_eventually_in Y

        proof

          take i;

          let j be Element of N;

          assume i <= j;

          then (N . j) in X by A2;

          hence thesis by A1;

        end;

      end;

      assume

       A3: for i be Element of N holds ex j be Element of N st i <= j & (N . j) in X;

      let i be Element of N;

      consider j be Element of N such that

       A4: i <= j and

       A5: (N . j) in X by A3;

      take j;

      thus thesis by A1, A4, A5;

    end;

    theorem :: WAYBEL_0:9

    for L be non empty 1-sorted, N be non empty NetStr over L holds for X be set holds N is_eventually_in X iff not N is_often_in (the carrier of L \ X)

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L, X be set;

      set Y = (the carrier of L \ X);

      thus N is_eventually_in X implies not N is_often_in Y

      proof

        given i be Element of N such that

         A1: for j be Element of N st i <= j holds (N . j) in X;

        take i;

        let j be Element of N;

        assume i <= j;

        then (N . j) in X by A1;

        hence thesis by XBOOLE_0:def 5;

      end;

      given i be Element of N such that

       A2: for j be Element of N st i <= j holds not (N . j) in Y;

      take i;

      let j be Element of N;

      assume i <= j;

      then not (N . j) in Y by A2;

      hence thesis by XBOOLE_0:def 5;

    end;

    theorem :: WAYBEL_0:10

    for L be non empty 1-sorted, N be non empty NetStr over L holds for X be set holds N is_often_in X iff not N is_eventually_in (the carrier of L \ X)

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L, X be set;

      set Y = (the carrier of L \ X);

      thus N is_often_in X implies not N is_eventually_in Y

      proof

        assume

         A1: for i be Element of N holds ex j be Element of N st i <= j & (N . j) in X;

        let i be Element of N;

        consider j be Element of N such that

         A2: i <= j and

         A3: (N . j) in X by A1;

        take j;

        thus thesis by A2, A3, XBOOLE_0:def 5;

      end;

      assume

       A4: for i be Element of N holds ex j be Element of N st i <= j & not (N . j) in Y;

      let i be Element of N;

      consider j be Element of N such that

       A5: i <= j and

       A6: not (N . j) in Y by A4;

      take j;

      thus thesis by A5, A6, XBOOLE_0:def 5;

    end;

    scheme :: WAYBEL_0:sch1

    HoldsEventually { L() -> non empty RelStr , N() -> non empty NetStr over L() , P[ set] } :

N() is_eventually_in { (N() . k) where k be Element of N() : P[(N() . k)] } iff ex i be Element of N() st for j be Element of N() st i <= j holds P[(N() . j)];

      set X = { (N() . k) where k be Element of N() : P[(N() . k)] };

      hereby

        assume N() is_eventually_in X;

        then

        consider i be Element of N() such that

         A1: for j be Element of N() st i <= j holds (N() . j) in X;

        take i;

        let j be Element of N();

        assume i <= j;

        then (N() . j) in X by A1;

        then ex k be Element of N() st (N() . j) = (N() . k) & P[(N() . k)];

        hence P[(N() . j)];

      end;

      given i be Element of N() such that

       A2: for j be Element of N() st i <= j holds P[(N() . j)];

      take i;

      let j be Element of N();

      assume i <= j;

      then P[(N() . j)] by A2;

      hence thesis;

    end;

    definition

      let L be non empty RelStr;

      let N be non empty NetStr over L;

      :: WAYBEL_0:def13

      attr N is eventually-directed means for i be Element of N holds N is_eventually_in { (N . j) where j be Element of N : (N . i) <= (N . j) };

      :: WAYBEL_0:def14

      attr N is eventually-filtered means for i be Element of N holds N is_eventually_in { (N . j) where j be Element of N : (N . i) >= (N . j) };

    end

    theorem :: WAYBEL_0:11

    

     Th11: for L be non empty RelStr, N be non empty NetStr over L holds N is eventually-directed iff for i be Element of N holds ex j be Element of N st for k be Element of N st j <= k holds (N . i) <= (N . k)

    proof

      let L be non empty RelStr, N be non empty NetStr over L;

       A1:

      now

        let i be Element of N;

        defpred P[ Element of L] means (N . i) <= $1;

        thus N is_eventually_in { (N . j) where j be Element of N : P[(N . j)] } iff ex k be Element of N st for l be Element of N st k <= l holds P[(N . l)] from HoldsEventually;

      end;

      hereby

        assume

         A2: N is eventually-directed;

        let i be Element of N;

        N is_eventually_in { (N . j) where j be Element of N : (N . i) <= (N . j) } by A2;

        hence ex j be Element of N st for k be Element of N st j <= k holds (N . i) <= (N . k) by A1;

      end;

      assume

       A3: for i be Element of N holds ex j be Element of N st for k be Element of N st j <= k holds (N . i) <= (N . k);

      let i be Element of N;

      ex j be Element of N st for k be Element of N st j <= k holds (N . i) <= (N . k) by A3;

      hence thesis by A1;

    end;

    theorem :: WAYBEL_0:12

    

     Th12: for L be non empty RelStr, N be non empty NetStr over L holds N is eventually-filtered iff for i be Element of N holds ex j be Element of N st for k be Element of N st j <= k holds (N . i) >= (N . k)

    proof

      let L be non empty RelStr, N be non empty NetStr over L;

       A1:

      now

        let i be Element of N;

        defpred P[ Element of L] means (N . i) >= $1;

        thus N is_eventually_in { (N . j) where j be Element of N : P[(N . j)] } iff ex k be Element of N st for l be Element of N st k <= l holds P[(N . l)] from HoldsEventually;

      end;

      hereby

        assume

         A2: N is eventually-filtered;

        let i be Element of N;

        N is_eventually_in { (N . j) where j be Element of N : (N . i) >= (N . j) } by A2;

        hence ex j be Element of N st for k be Element of N st j <= k holds (N . i) >= (N . k) by A1;

      end;

      assume

       A3: for i be Element of N holds ex j be Element of N st for k be Element of N st j <= k holds (N . i) >= (N . k);

      let i be Element of N;

      ex j be Element of N st for k be Element of N st j <= k holds (N . i) >= (N . k) by A3;

      hence thesis by A1;

    end;

    registration

      let L be non empty RelStr;

      cluster monotone -> eventually-directed for prenet of L;

      coherence

      proof

        let N be prenet of L;

        assume

         A1: for i,j be Element of N st i <= j holds for a,b be Element of L st a = (( netmap (N,L)) . i) & b = (( netmap (N,L)) . j) holds a <= b;

        now

          let i be Element of N;

          take j = i;

          let k be Element of N;

          assume j <= k;

          hence (N . i) <= (N . k) by A1;

        end;

        hence thesis by Th11;

      end;

      cluster antitone -> eventually-filtered for prenet of L;

      coherence

      proof

        let N be prenet of L;

        assume

         A2: for i,j be Element of N st i <= j holds for a,b be Element of L st a = (( netmap (N,L)) . i) & b = (( netmap (N,L)) . j) holds a >= b;

        now

          let i be Element of N;

          take j = i;

          let k be Element of N;

          assume j <= k;

          hence (N . i) >= (N . k) by A2;

        end;

        hence thesis by Th12;

      end;

    end

    registration

      let L be non empty reflexive RelStr;

      cluster monotone antitone strict for prenet of L;

      existence

      proof

        set J = the upper-bounded non empty Poset;

        set x = the Element of L;

        set M = (the carrier of J --> x);

        reconsider M as Function of the carrier of J, the carrier of L;

        set N = NetStr (# the carrier of J, the InternalRel of J, M #);

        

         A1: the RelStr of N = the RelStr of J;

        ( [#] J) = ( [#] N);

        then ( [#] N) is directed by A1, Th3;

        then

        reconsider N as prenet of L by Def6;

        take N;

        thus N is monotone

        proof

          let i,j be Element of N such that i <= j;

          let a,b be Element of L;

          assume that

           A2: a = (( netmap (N,L)) . i) and

           A3: b = (( netmap (N,L)) . j);

          

           A4: a = x by A2, FUNCOP_1: 7;

          x <= x;

          hence thesis by A3, A4, FUNCOP_1: 7;

        end;

        thus N is antitone

        proof

          let i,j be Element of N such that i <= j;

          let a,b be Element of L;

          assume that

           A5: a = (( netmap (N,L)) . i) and

           A6: b = (( netmap (N,L)) . j);

          

           A7: a = x by A5, FUNCOP_1: 7;

          x <= x;

          hence thesis by A6, A7, FUNCOP_1: 7;

        end;

        thus thesis;

      end;

    end

    begin

    definition

      let L be RelStr;

      let X be Subset of L;

      :: WAYBEL_0:def15

      func downarrow X -> Subset of L means

      : Def15: for x be Element of L holds x in it iff ex y be Element of L st y >= x & y in X;

      existence

      proof

        defpred P[ object] means ex a,y be Element of L st a = $1 & y >= a & y in X;

        consider S be set such that

         A1: for x be object holds x in S iff x in the carrier of L & P[x] from XBOOLE_0:sch 1;

        S c= the carrier of L by A1;

        then

        reconsider S as Subset of L;

        take S;

        let x be Element of L;

        hereby

          assume x in S;

          then ex a,y be Element of L st a = x & y >= a & y in X by A1;

          hence ex y be Element of L st y >= x & y in X;

        end;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let S1,S2 be Subset of L such that

         A2: for x be Element of L holds x in S1 iff ex y be Element of L st y >= x & y in X and

         A3: for x be Element of L holds x in S2 iff ex y be Element of L st y >= x & y in X;

        thus S1 c= S2

        proof

          let x be object;

          assume

           A4: x in S1;

          then

          reconsider x as Element of L;

          ex y be Element of L st y >= x & y in X by A2, A4;

          hence thesis by A3;

        end;

        let x be object;

        assume

         A5: x in S2;

        then

        reconsider x as Element of L;

        ex y be Element of L st y >= x & y in X by A3, A5;

        hence thesis by A2;

      end;

      :: WAYBEL_0:def16

      func uparrow X -> Subset of L means

      : Def16: for x be Element of L holds x in it iff ex y be Element of L st y <= x & y in X;

      existence

      proof

        defpred P[ object] means ex a,y be Element of L st a = $1 & y <= a & y in X;

        consider S be set such that

         A6: for x be object holds x in S iff x in the carrier of L & P[x] from XBOOLE_0:sch 1;

        S c= the carrier of L by A6;

        then

        reconsider S as Subset of L;

        take S;

        let x be Element of L;

        hereby

          assume x in S;

          then ex a,y be Element of L st a = x & y <= a & y in X by A6;

          hence ex y be Element of L st y <= x & y in X;

        end;

        thus thesis by A6;

      end;

      correctness

      proof

        let S1,S2 be Subset of L such that

         A7: for x be Element of L holds x in S1 iff ex y be Element of L st y <= x & y in X and

         A8: for x be Element of L holds x in S2 iff ex y be Element of L st y <= x & y in X;

        thus S1 c= S2

        proof

          let x be object;

          assume

           A9: x in S1;

          then

          reconsider x as Element of L;

          ex y be Element of L st y <= x & y in X by A7, A9;

          hence thesis by A8;

        end;

        let x be object;

        assume

         A10: x in S2;

        then

        reconsider x as Element of L;

        ex y be Element of L st y <= x & y in X by A8, A10;

        hence thesis by A7;

      end;

    end

    theorem :: WAYBEL_0:13

    

     Th13: for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 holds for X be Subset of L1 holds for Y be Subset of L2 st X = Y holds ( downarrow X) = ( downarrow Y) & ( uparrow X) = ( uparrow Y)

    proof

      let L1,L2 be RelStr such that

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

      let X be Subset of L1;

      let Y be Subset of L2 such that

       A2: X = Y;

      thus ( downarrow X) c= ( downarrow Y)

      proof

        let x be object;

        assume

         A3: x in ( downarrow X);

        then

        reconsider x as Element of L1;

        reconsider x9 = x as Element of L2 by A1;

        consider y be Element of L1 such that

         A4: y >= x and

         A5: y in X by A3, Def15;

        reconsider y9 = y as Element of L2 by A1;

        y9 >= x9 by A1, A4, YELLOW_0: 1;

        hence thesis by A2, A5, Def15;

      end;

      thus ( downarrow Y) c= ( downarrow X)

      proof

        let x be object;

        assume

         A6: x in ( downarrow Y);

        then

        reconsider x as Element of L2;

        reconsider x9 = x as Element of L1 by A1;

        consider y be Element of L2 such that

         A7: y >= x and

         A8: y in Y by A6, Def15;

        reconsider y9 = y as Element of L1 by A1;

        y9 >= x9 by A1, A7, YELLOW_0: 1;

        hence thesis by A2, A8, Def15;

      end;

      thus ( uparrow X) c= ( uparrow Y)

      proof

        let x be object;

        assume

         A9: x in ( uparrow X);

        then

        reconsider x as Element of L1;

        reconsider x9 = x as Element of L2 by A1;

        consider y be Element of L1 such that

         A10: y <= x and

         A11: y in X by A9, Def16;

        reconsider y9 = y as Element of L2 by A1;

        y9 <= x9 by A1, A10, YELLOW_0: 1;

        hence thesis by A2, A11, Def16;

      end;

      thus ( uparrow Y) c= ( uparrow X)

      proof

        let x be object;

        assume

         A12: x in ( uparrow Y);

        then

        reconsider x as Element of L2;

        reconsider x9 = x as Element of L1 by A1;

        consider y be Element of L2 such that

         A13: y <= x and

         A14: y in Y by A12, Def16;

        reconsider y9 = y as Element of L1 by A1;

        y9 <= x9 by A1, A13, YELLOW_0: 1;

        hence thesis by A2, A14, Def16;

      end;

    end;

    theorem :: WAYBEL_0:14

    

     Th14: for L be non empty RelStr, X be Subset of L holds ( downarrow X) = { x where x be Element of L : ex y be Element of L st x <= y & y in X }

    proof

      let L be non empty RelStr, X be Subset of L;

      set Y = { x where x be Element of L : ex y be Element of L st x <= y & y in X };

      hereby

        let x be object;

        assume

         A1: x in ( downarrow X);

        then

        reconsider y = x as Element of L;

        ex z be Element of L st z >= y & z in X by A1, Def15;

        hence x in Y;

      end;

      let x be object;

      assume x in Y;

      then ex a be Element of L st a = x & ex y be Element of L st a <= y & y in X;

      hence thesis by Def15;

    end;

    theorem :: WAYBEL_0:15

    

     Th15: for L be non empty RelStr, X be Subset of L holds ( uparrow X) = { x where x be Element of L : ex y be Element of L st x >= y & y in X }

    proof

      let L be non empty RelStr, X be Subset of L;

      set Y = { x where x be Element of L : ex y be Element of L st x >= y & y in X };

      hereby

        let x be object;

        assume

         A1: x in ( uparrow X);

        then

        reconsider y = x as Element of L;

        ex z be Element of L st z <= y & z in X by A1, Def16;

        hence x in Y;

      end;

      let x be object;

      assume x in Y;

      then ex a be Element of L st a = x & ex y be Element of L st a >= y & y in X;

      hence thesis by Def16;

    end;

    registration

      let L be non empty reflexive RelStr;

      let X be non empty Subset of L;

      cluster ( downarrow X) -> non empty;

      coherence

      proof

        set x = the Element of X;

        reconsider x9 = x as Element of L;

        x9 <= x9;

        hence thesis by Def15;

      end;

      cluster ( uparrow X) -> non empty;

      coherence

      proof

        set x = the Element of X;

        reconsider x9 = x as Element of L;

        x9 <= x9;

        hence thesis by Def16;

      end;

    end

    theorem :: WAYBEL_0:16

    

     Th16: for L be reflexive RelStr, X be Subset of L holds X c= ( downarrow X) & X c= ( uparrow X)

    proof

      let L be reflexive RelStr, X be Subset of L;

      

       A1: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def 2;

      hereby

        let x be object;

        assume

         A2: x in X;

        then

        reconsider y = x as Element of L;

         [y, y] in the InternalRel of L by A1, A2, RELAT_2:def 1;

        then y <= y by ORDERS_2:def 5;

        hence x in ( downarrow X) by A2, Def15;

      end;

      let x be object;

      assume

       A3: x in X;

      then

      reconsider y = x as Element of L;

       [y, y] in the InternalRel of L by A1, A3, RELAT_2:def 1;

      then y <= y by ORDERS_2:def 5;

      hence thesis by A3, Def16;

    end;

    definition

      let L be non empty RelStr;

      let x be Element of L;

      :: WAYBEL_0:def17

      func downarrow x -> Subset of L equals ( downarrow {x});

      correctness ;

      :: WAYBEL_0:def18

      func uparrow x -> Subset of L equals ( uparrow {x});

      correctness ;

    end

    theorem :: WAYBEL_0:17

    

     Th17: for L be non empty RelStr, x,y be Element of L holds y in ( downarrow x) iff y <= x

    proof

      let L be non empty RelStr, x,y be Element of L;

      

       A1: ( downarrow x) = { z where z be Element of L : ex v be Element of L st z <= v & v in {x} } by Th14;

      then y in ( downarrow x) iff ex z be Element of L st y = z & ex v be Element of L st z <= v & v in {x};

      hence y in ( downarrow x) implies y <= x by TARSKI:def 1;

      x in {x} by TARSKI:def 1;

      hence thesis by A1;

    end;

    theorem :: WAYBEL_0:18

    

     Th18: for L be non empty RelStr, x,y be Element of L holds y in ( uparrow x) iff x <= y

    proof

      let L be non empty RelStr, x,y be Element of L;

      

       A1: ( uparrow x) = { z where z be Element of L : ex v be Element of L st z >= v & v in {x} } by Th15;

      then y in ( uparrow x) iff ex z be Element of L st y = z & ex v be Element of L st z >= v & v in {x};

      hence y in ( uparrow x) implies y >= x by TARSKI:def 1;

      x in {x} by TARSKI:def 1;

      hence thesis by A1;

    end;

    theorem :: WAYBEL_0:19

    for L be non empty reflexive antisymmetric RelStr holds for x,y be Element of L st ( downarrow x) = ( downarrow y) holds x = y

    proof

      let L be non empty reflexive antisymmetric RelStr;

      let x,y be Element of L;

      reconsider x9 = x, y9 = y as Element of L;

      

       A1: x9 <= x9;

      

       A2: y9 <= y9;

      assume

       A3: ( downarrow x) = ( downarrow y);

      then

       A4: y in ( downarrow x) by A2, Th17;

      x in ( downarrow y) by A1, A3, Th17;

      then

       A5: x9 <= y9 by Th17;

      x9 >= y9 by A4, Th17;

      hence thesis by A5, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_0:20

    for L be non empty reflexive antisymmetric RelStr holds for x,y be Element of L st ( uparrow x) = ( uparrow y) holds x = y

    proof

      let L be non empty reflexive antisymmetric RelStr;

      let x,y be Element of L;

      reconsider x9 = x, y9 = y as Element of L;

      

       A1: x9 <= x9;

      

       A2: y9 <= y9;

      assume

       A3: ( uparrow x) = ( uparrow y);

      then

       A4: y in ( uparrow x) by A2, Th18;

      

       A5: x in ( uparrow y) by A1, A3, Th18;

      

       A6: x9 <= y9 by A4, Th18;

      x9 >= y9 by A5, Th18;

      hence thesis by A6, ORDERS_2: 2;

    end;

    theorem :: WAYBEL_0:21

    

     Th21: for L be non empty transitive RelStr holds for x,y be Element of L st x <= y holds ( downarrow x) c= ( downarrow y)

    proof

      let L be non empty transitive RelStr;

      let x,y be Element of L such that

       A1: x <= y;

      let z be object;

      assume

       A2: z in ( downarrow x);

      then

      reconsider z as Element of L;

      z <= x by A2, Th17;

      then z <= y by A1, ORDERS_2: 3;

      hence thesis by Th17;

    end;

    theorem :: WAYBEL_0:22

    

     Th22: for L be non empty transitive RelStr holds for x,y be Element of L st x <= y holds ( uparrow y) c= ( uparrow x)

    proof

      let L be non empty transitive RelStr;

      let x,y be Element of L such that

       A1: x <= y;

      let z be object;

      assume

       A2: z in ( uparrow y);

      then

      reconsider z as Element of L;

      y <= z by A2, Th18;

      then x <= z by A1, ORDERS_2: 3;

      hence thesis by Th18;

    end;

    registration

      let L be non empty reflexive RelStr;

      let x be Element of L;

      cluster ( downarrow x) -> non empty directed;

      coherence

      proof

        reconsider x9 = x as Element of L;

        thus ( downarrow x) is non empty;

        let z,y be Element of L;

        assume that

         A1: z in ( downarrow x) and

         A2: y in ( downarrow x);

        take x9;

        x9 <= x9;

        hence x9 in ( downarrow x) & z <= x9 & y <= x9 by A1, A2, Th17;

      end;

      cluster ( uparrow x) -> non empty filtered;

      coherence

      proof

        reconsider x9 = x as Element of L;

        thus ( uparrow x) is non empty;

        let z,y be Element of L;

        assume that

         A3: z in ( uparrow x) and

         A4: y in ( uparrow x);

        take x9;

        x9 <= x9;

        hence x9 in ( uparrow x) & x9 <= z & x9 <= y by A3, A4, Th18;

      end;

    end

    definition

      let L be RelStr;

      let X be Subset of L;

      :: WAYBEL_0:def19

      attr X is lower means

      : Def19: for x,y be Element of L st x in X & y <= x holds y in X;

      :: WAYBEL_0:def20

      attr X is upper means

      : Def20: for x,y be Element of L st x in X & x <= y holds y in X;

    end

    registration

      let L be RelStr;

      cluster lower upper for Subset of L;

      existence

      proof

        the carrier of L c= the carrier of L;

        then

        reconsider S = the carrier of L as Subset of L;

        take S;

        thus S is lower;

        let x be Element of L;

        thus thesis;

      end;

    end

    theorem :: WAYBEL_0:23

    

     Th23: for L be RelStr, X be Subset of L holds X is lower iff ( downarrow X) c= X

    proof

      let L be RelStr, X be Subset of L;

      hereby

        assume

         A1: X is lower;

        thus ( downarrow X) c= X

        proof

          let x be object;

          assume

           A2: x in ( downarrow X);

          then

          reconsider x9 = x as Element of L;

          ex y be Element of L st x9 <= y & y in X by A2, Def15;

          hence thesis by A1;

        end;

      end;

      assume

       A3: ( downarrow X) c= X;

      let x,y be Element of L;

      assume that

       A4: x in X and

       A5: y <= x;

      y in ( downarrow X) by A4, A5, Def15;

      hence thesis by A3;

    end;

    theorem :: WAYBEL_0:24

    

     Th24: for L be RelStr, X be Subset of L holds X is upper iff ( uparrow X) c= X

    proof

      let L be RelStr, X be Subset of L;

      hereby

        assume

         A1: X is upper;

        thus ( uparrow X) c= X

        proof

          let x be object;

          assume

           A2: x in ( uparrow X);

          then

          reconsider x9 = x as Element of L;

          ex y be Element of L st x9 >= y & y in X by A2, Def16;

          hence thesis by A1;

        end;

      end;

      assume

       A3: ( uparrow X) c= X;

      let x,y be Element of L;

      assume that

       A4: x in X and

       A5: y >= x;

      y in ( uparrow X) by A4, A5, Def16;

      hence thesis by A3;

    end;

    theorem :: WAYBEL_0:25

    for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 holds for X1 be Subset of L1, X2 be Subset of L2 st X1 = X2 holds (X1 is lower implies X2 is lower) & (X1 is upper implies X2 is upper)

    proof

      let L1,L2 be RelStr such that

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

      let X1 be Subset of L1, X2 be Subset of L2;

      assume

       A2: X1 = X2;

      hereby

        assume

         A3: X1 is lower;

        

         A4: ( downarrow X1) = ( downarrow X2) by A1, A2, Th13;

        ( downarrow X1) c= X1 by A3, Th23;

        hence X2 is lower by A2, A4, Th23;

      end;

      assume

       A5: X1 is upper;

      

       A6: ( uparrow X1) = ( uparrow X2) by A1, A2, Th13;

      ( uparrow X1) c= X1 by A5, Th24;

      hence thesis by A2, A6, Th24;

    end;

    theorem :: WAYBEL_0:26

    for L be RelStr, A be Subset-Family of L st for X be Subset of L st X in A holds X is lower holds ( union A) is lower Subset of L

    proof

      let L be RelStr, A be Subset-Family of L such that

       A1: for X be Subset of L st X in A holds X is lower;

      reconsider A as Subset-Family of L;

      reconsider X = ( union A) as Subset of L;

      X is lower

      proof

        let x,y be Element of L;

        assume x in X;

        then

        consider Y be set such that

         A2: x in Y and

         A3: Y in A by TARSKI:def 4;

        reconsider Y as Subset of L by A3;

        

         A4: Y is lower by A1, A3;

        assume y <= x;

        then y in Y by A2, A4;

        hence thesis by A3, TARSKI:def 4;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_0:27

    

     Th27: for L be RelStr, X,Y be Subset of L st X is lower & Y is lower holds (X /\ Y) is lower & (X \/ Y) is lower

    proof

      let L be RelStr;

      let X,Y be Subset of L such that

       A1: for x,y be Element of L st x in X & y <= x holds y in X and

       A2: for x,y be Element of L st x in Y & y <= x holds y in Y;

      hereby

        let x,y be Element of L;

        assume

         A3: x in (X /\ Y);

        then

         A4: x in X by XBOOLE_0:def 4;

        

         A5: x in Y by A3, XBOOLE_0:def 4;

        assume

         A6: y <= x;

        then

         A7: y in X by A1, A4;

        y in Y by A2, A5, A6;

        hence y in (X /\ Y) by A7, XBOOLE_0:def 4;

      end;

      let x,y be Element of L;

      assume x in (X \/ Y);

      then

       A8: x in X or x in Y by XBOOLE_0:def 3;

      assume y <= x;

      then y in X or y in Y by A1, A2, A8;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: WAYBEL_0:28

    for L be RelStr, A be Subset-Family of L st for X be Subset of L st X in A holds X is upper holds ( union A) is upper Subset of L

    proof

      let L be RelStr, A be Subset-Family of L such that

       A1: for X be Subset of L st X in A holds X is upper;

      reconsider A as Subset-Family of L;

      reconsider X = ( union A) as Subset of L;

      X is upper

      proof

        let x,y be Element of L;

        assume x in X;

        then

        consider Y be set such that

         A2: x in Y and

         A3: Y in A by TARSKI:def 4;

        reconsider Y as Subset of L by A3;

        

         A4: Y is upper by A1, A3;

        assume y >= x;

        then y in Y by A2, A4;

        hence thesis by A3, TARSKI:def 4;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_0:29

    

     Th29: for L be RelStr, X,Y be Subset of L st X is upper & Y is upper holds (X /\ Y) is upper & (X \/ Y) is upper

    proof

      let L be RelStr;

      let X,Y be Subset of L such that

       A1: for x,y be Element of L st x in X & y >= x holds y in X and

       A2: for x,y be Element of L st x in Y & y >= x holds y in Y;

      hereby

        let x,y be Element of L;

        assume

         A3: x in (X /\ Y);

        then

         A4: x in X by XBOOLE_0:def 4;

        

         A5: x in Y by A3, XBOOLE_0:def 4;

        assume

         A6: y >= x;

        then

         A7: y in X by A1, A4;

        y in Y by A2, A5, A6;

        hence y in (X /\ Y) by A7, XBOOLE_0:def 4;

      end;

      let x,y be Element of L;

      assume x in (X \/ Y);

      then

       A8: x in X or x in Y by XBOOLE_0:def 3;

      assume y >= x;

      then y in X or y in Y by A1, A2, A8;

      hence thesis by XBOOLE_0:def 3;

    end;

    registration

      let L be non empty transitive RelStr;

      let X be Subset of L;

      cluster ( downarrow X) -> lower;

      coherence

      proof

        let y,z be Element of L;

        assume y in ( downarrow X);

        then

        consider x be Element of L such that

         A1: y <= x and

         A2: x in X by Def15;

        assume z <= y;

        then z <= x by A1, ORDERS_2: 3;

        hence thesis by A2, Def15;

      end;

      cluster ( uparrow X) -> upper;

      coherence

      proof

        let y,z be Element of L;

        assume y in ( uparrow X);

        then

        consider x be Element of L such that

         A3: y >= x and

         A4: x in X by Def16;

        assume z >= y;

        then z >= x by A3, ORDERS_2: 3;

        hence thesis by A4, Def16;

      end;

    end

    registration

      let L be non empty transitive RelStr;

      let x be Element of L;

      cluster ( downarrow x) -> lower;

      coherence ;

      cluster ( uparrow x) -> upper;

      coherence ;

    end

    registration

      let L be non empty RelStr;

      cluster ( [#] L) -> lower upper;

      coherence ;

    end

    registration

      let L be non empty RelStr;

      cluster non empty lower upper for Subset of L;

      existence

      proof

        take ( [#] L);

        thus thesis;

      end;

    end

    registration

      let L be non empty reflexive transitive RelStr;

      cluster non empty lower directed for Subset of L;

      existence

      proof

        set x = the Element of L;

        take ( downarrow x);

        thus thesis;

      end;

      cluster non empty upper filtered for Subset of L;

      existence

      proof

        set x = the Element of L;

        take ( uparrow x);

        thus thesis;

      end;

    end

    registration

      let L be with_infima with_suprema Poset;

      cluster non empty directed filtered lower upper for Subset of L;

      existence

      proof

        take ( [#] L);

        thus thesis;

      end;

    end

    theorem :: WAYBEL_0:30

    

     Th30: for L be non empty transitive reflexive RelStr, X be Subset of L holds X is directed iff ( downarrow X) is directed

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      thus X is directed implies ( downarrow X) is directed

      proof

        assume

         A1: for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x <= z & y <= z;

        let x,y be Element of L;

        assume that

         A2: x in ( downarrow X) and

         A3: y in ( downarrow X);

        consider x9 be Element of L such that

         A4: x <= x9 and

         A5: x9 in X by A2, Def15;

        consider y9 be Element of L such that

         A6: y <= y9 and

         A7: y9 in X by A3, Def15;

        consider z be Element of L such that

         A8: z in X and

         A9: x9 <= z and

         A10: y9 <= z by A1, A5, A7;

        take z;

        z <= z;

        hence z in ( downarrow X) by A8, Def15;

        thus thesis by A4, A6, A9, A10, ORDERS_2: 3;

      end;

      set Y = ( downarrow X);

      assume

       A11: for x,y be Element of L st x in Y & y in Y holds ex z be Element of L st z in Y & x <= z & y <= z;

      let x,y be Element of L;

      assume that

       A12: x in X and

       A13: y in X;

      

       A14: x <= x;

      

       A15: y <= y;

      

       A16: x in Y by A12, A14, Def15;

      y in Y by A13, A15, Def15;

      then

      consider z be Element of L such that

       A17: z in Y and

       A18: x <= z and

       A19: y <= z by A11, A16;

      consider z9 be Element of L such that

       A20: z <= z9 and

       A21: z9 in X by A17, Def15;

      take z9;

      thus z9 in X by A21;

      thus thesis by A18, A19, A20, ORDERS_2: 3;

    end;

    registration

      let L be non empty transitive reflexive RelStr;

      let X be directed Subset of L;

      cluster ( downarrow X) -> directed;

      coherence by Th30;

    end

    theorem :: WAYBEL_0:31

    

     Th31: for L be non empty transitive reflexive RelStr, X be Subset of L holds for x be Element of L holds x is_>=_than X iff x is_>=_than ( downarrow X)

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      let x be Element of L;

      thus x is_>=_than X implies x is_>=_than ( downarrow X)

      proof

        assume

         A1: for y be Element of L st y in X holds x >= y;

        let y be Element of L;

        assume y in ( downarrow X);

        then

        consider z be Element of L such that

         A2: y <= z and

         A3: z in X by Def15;

        x >= z by A1, A3;

        hence thesis by A2, ORDERS_2: 3;

      end;

      assume

       A4: for y be Element of L st y in ( downarrow X) holds x >= y;

      let y be Element of L;

      assume

       A5: y in X;

      y <= y;

      then y in ( downarrow X) by A5, Def15;

      hence thesis by A4;

    end;

    theorem :: WAYBEL_0:32

    

     Th32: for L be non empty transitive reflexive RelStr, X be Subset of L holds ex_sup_of (X,L) iff ex_sup_of (( downarrow X),L)

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      for x be Element of L holds x is_>=_than X iff x is_>=_than ( downarrow X) by Th31;

      hence thesis by YELLOW_0: 46;

    end;

    theorem :: WAYBEL_0:33

    

     Th33: for L be non empty transitive reflexive RelStr, X be Subset of L st ex_sup_of (X,L) holds ( sup X) = ( sup ( downarrow X))

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      for x be Element of L holds x is_>=_than X iff x is_>=_than ( downarrow X) by Th31;

      hence thesis by YELLOW_0: 47;

    end;

    theorem :: WAYBEL_0:34

    for L be non empty Poset, x be Element of L holds ex_sup_of (( downarrow x),L) & ( sup ( downarrow x)) = x

    proof

      let L be non empty Poset, x be Element of L;

       ex_sup_of ( {x},L) by YELLOW_0: 38;

      hence ex_sup_of (( downarrow x),L) by Th32;

      

      thus ( sup ( downarrow x)) = ( sup {x}) by Th33, YELLOW_0: 38

      .= x by YELLOW_0: 39;

    end;

    theorem :: WAYBEL_0:35

    

     Th35: for L be non empty transitive reflexive RelStr, X be Subset of L holds X is filtered iff ( uparrow X) is filtered

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      thus X is filtered implies ( uparrow X) is filtered

      proof

        assume

         A1: for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x >= z & y >= z;

        let x,y be Element of L;

        assume that

         A2: x in ( uparrow X) and

         A3: y in ( uparrow X);

        consider x9 be Element of L such that

         A4: x >= x9 and

         A5: x9 in X by A2, Def16;

        consider y9 be Element of L such that

         A6: y >= y9 and

         A7: y9 in X by A3, Def16;

        consider z be Element of L such that

         A8: z in X and

         A9: x9 >= z and

         A10: y9 >= z by A1, A5, A7;

        take z;

        z >= z by ORDERS_2: 1;

        hence z in ( uparrow X) by A8, Def16;

        thus thesis by A4, A6, A9, A10, ORDERS_2: 3;

      end;

      set Y = ( uparrow X);

      assume

       A11: for x,y be Element of L st x in Y & y in Y holds ex z be Element of L st z in Y & x >= z & y >= z;

      let x,y be Element of L;

      assume that

       A12: x in X and

       A13: y in X;

      

       A14: x >= x by ORDERS_2: 1;

      

       A15: y >= y by ORDERS_2: 1;

      

       A16: x in Y by A12, A14, Def16;

      y in Y by A13, A15, Def16;

      then

      consider z be Element of L such that

       A17: z in Y and

       A18: x >= z and

       A19: y >= z by A11, A16;

      consider z9 be Element of L such that

       A20: z >= z9 and

       A21: z9 in X by A17, Def16;

      take z9;

      thus z9 in X by A21;

      thus thesis by A18, A19, A20, ORDERS_2: 3;

    end;

    registration

      let L be non empty transitive reflexive RelStr;

      let X be filtered Subset of L;

      cluster ( uparrow X) -> filtered;

      coherence by Th35;

    end

    theorem :: WAYBEL_0:36

    

     Th36: for L be non empty transitive reflexive RelStr, X be Subset of L holds for x be Element of L holds x is_<=_than X iff x is_<=_than ( uparrow X)

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      let x be Element of L;

      thus x is_<=_than X implies x is_<=_than ( uparrow X)

      proof

        assume

         A1: for y be Element of L st y in X holds x <= y;

        let y be Element of L;

        assume y in ( uparrow X);

        then

        consider z be Element of L such that

         A2: y >= z and

         A3: z in X by Def16;

        x <= z by A1, A3;

        hence thesis by A2, ORDERS_2: 3;

      end;

      assume

       A4: for y be Element of L st y in ( uparrow X) holds x <= y;

      let y be Element of L;

      assume

       A5: y in X;

      y <= y;

      then y in ( uparrow X) by A5, Def16;

      hence thesis by A4;

    end;

    theorem :: WAYBEL_0:37

    

     Th37: for L be non empty transitive reflexive RelStr, X be Subset of L holds ex_inf_of (X,L) iff ex_inf_of (( uparrow X),L)

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      for x be Element of L holds x is_<=_than X iff x is_<=_than ( uparrow X) by Th36;

      hence thesis by YELLOW_0: 48;

    end;

    theorem :: WAYBEL_0:38

    

     Th38: for L be non empty transitive reflexive RelStr, X be Subset of L st ex_inf_of (X,L) holds ( inf X) = ( inf ( uparrow X))

    proof

      let L be non empty transitive reflexive RelStr, X be Subset of L;

      for x be Element of L holds x is_<=_than X iff x is_<=_than ( uparrow X) by Th36;

      hence thesis by YELLOW_0: 49;

    end;

    theorem :: WAYBEL_0:39

    for L be non empty Poset, x be Element of L holds ex_inf_of (( uparrow x),L) & ( inf ( uparrow x)) = x

    proof

      let L be non empty Poset, x be Element of L;

       ex_inf_of ( {x},L) by YELLOW_0: 38;

      hence ex_inf_of (( uparrow x),L) by Th37;

      

      thus ( inf ( uparrow x)) = ( inf {x}) by Th38, YELLOW_0: 38

      .= x by YELLOW_0: 39;

    end;

    begin

    definition

      let L be non empty reflexive transitive RelStr;

      mode Ideal of L is directed lower non empty Subset of L;

      mode Filter of L is filtered upper non empty Subset of L;

    end

    theorem :: WAYBEL_0:40

    

     Th40: for L be with_suprema antisymmetric RelStr, X be lower Subset of L holds X is directed iff for x,y be Element of L st x in X & y in X holds (x "\/" y) in X

    proof

      let L be with_suprema antisymmetric RelStr, X be lower Subset of L;

      thus X is directed implies for x,y be Element of L st x in X & y in X holds (x "\/" y) in X

      proof

        assume

         A1: for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x <= z & y <= z;

        let x,y be Element of L;

        assume that

         A2: x in X and

         A3: y in X;

        consider z be Element of L such that

         A4: z in X and

         A5: x <= z and

         A6: y <= z by A1, A2, A3;

        (x "\/" y) <= z by A5, A6, YELLOW_0: 22;

        hence thesis by A4, Def19;

      end;

      assume

       A7: for x,y be Element of L st x in X & y in X holds (x "\/" y) in X;

      let x,y be Element of L;

      assume that

       A8: x in X and

       A9: y in X;

      

       A10: x <= (x "\/" y) by YELLOW_0: 22;

      y <= (x "\/" y) by YELLOW_0: 22;

      hence thesis by A7, A8, A9, A10;

    end;

    theorem :: WAYBEL_0:41

    

     Th41: for L be with_infima antisymmetric RelStr, X be upper Subset of L holds X is filtered iff for x,y be Element of L st x in X & y in X holds (x "/\" y) in X

    proof

      let L be with_infima antisymmetric RelStr, X be upper Subset of L;

      thus X is filtered implies for x,y be Element of L st x in X & y in X holds (x "/\" y) in X

      proof

        assume

         A1: for x,y be Element of L st x in X & y in X holds ex z be Element of L st z in X & x >= z & y >= z;

        let x,y be Element of L;

        assume that

         A2: x in X and

         A3: y in X;

        consider z be Element of L such that

         A4: z in X and

         A5: x >= z and

         A6: y >= z by A1, A2, A3;

        (x "/\" y) >= z by A5, A6, YELLOW_0: 23;

        hence thesis by A4, Def20;

      end;

      assume

       A7: for x,y be Element of L st x in X & y in X holds (x "/\" y) in X;

      let x,y be Element of L;

      assume that

       A8: x in X and

       A9: y in X;

      

       A10: x >= (x "/\" y) by YELLOW_0: 23;

      y >= (x "/\" y) by YELLOW_0: 23;

      hence thesis by A7, A8, A9, A10;

    end;

    theorem :: WAYBEL_0:42

    

     Th42: for L be with_suprema Poset holds for X be non empty lower Subset of L holds X is directed iff for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in X

    proof

      let L be with_suprema Poset;

      let X be non empty lower Subset of L;

      thus X is directed implies for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in X

      proof

        assume

         A1: X is directed;

        let Y be finite Subset of X such that

         A2: Y <> {} ;

        consider z be Element of L such that

         A3: z in X and

         A4: Y is_<=_than z by A1, Th1;

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

        then ex_sup_of (Y,L) by A2, YELLOW_0: 54;

        then ( "\/" (Y,L)) <= z by A4, YELLOW_0: 30;

        hence thesis by A3, Def19;

      end;

      assume

       A5: for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in X;

      set x = the Element of X;

      reconsider x as Element of L;

      now

        let Y be finite Subset of X;

        per cases ;

          suppose Y = {} ;

          then x is_>=_than Y;

          hence ex x be Element of L st x in X & x is_>=_than Y;

        end;

          suppose

           A6: Y <> {} ;

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

          then ex_sup_of (Y,L) by A6, YELLOW_0: 54;

          then ( "\/" (Y,L)) is_>=_than Y by YELLOW_0: 30;

          hence ex x be Element of L st x in X & x is_>=_than Y by A5, A6;

        end;

      end;

      hence thesis by Th1;

    end;

    theorem :: WAYBEL_0:43

    

     Th43: for L be with_infima Poset holds for X be non empty upper Subset of L holds X is filtered iff for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in X

    proof

      let L be with_infima Poset, X be non empty upper Subset of L;

      thus X is filtered implies for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in X

      proof

        assume

         A1: X is filtered;

        let Y be finite Subset of X such that

         A2: Y <> {} ;

        consider z be Element of L such that

         A3: z in X and

         A4: Y is_>=_than z by A1, Th2;

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

        then ex_inf_of (Y,L) by A2, YELLOW_0: 55;

        then ( "/\" (Y,L)) >= z by A4, YELLOW_0: 31;

        hence thesis by A3, Def20;

      end;

      assume

       A5: for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in X;

      set x = the Element of X;

      reconsider x as Element of L;

      now

        let Y be finite Subset of X;

        per cases ;

          suppose Y = {} ;

          then x is_<=_than Y;

          hence ex x be Element of L st x in X & x is_<=_than Y;

        end;

          suppose

           A6: Y <> {} ;

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

          then ex_inf_of (Y,L) by A6, YELLOW_0: 55;

          then ( "/\" (Y,L)) is_<=_than Y by YELLOW_0: 31;

          hence ex x be Element of L st x in X & x is_<=_than Y by A5, A6;

        end;

      end;

      hence thesis by Th2;

    end;

    theorem :: WAYBEL_0:44

    for L be non empty antisymmetric RelStr st L is with_suprema or L is with_infima holds for X,Y be Subset of L st X is lower directed & Y is lower directed holds (X /\ Y) is directed

    proof

      let L be non empty antisymmetric RelStr such that

       A1: L is with_suprema or L is with_infima;

      let X,Y be Subset of L such that

       A2: X is lower directed and

       A3: Y is lower directed;

      

       A4: (X /\ Y) is lower by A2, A3, Th27;

      per cases by A1;

        suppose

         A5: L is with_suprema;

        now

          let x,y be Element of L;

          assume that

           A6: x in (X /\ Y) and

           A7: y in (X /\ Y);

          

           A8: x in X by A6, XBOOLE_0:def 4;

          

           A9: x in Y by A6, XBOOLE_0:def 4;

          

           A10: y in X by A7, XBOOLE_0:def 4;

          

           A11: y in Y by A7, XBOOLE_0:def 4;

          

           A12: (x "\/" y) in X by A2, A5, A8, A10, Th40;

          (x "\/" y) in Y by A3, A5, A9, A11, Th40;

          hence (x "\/" y) in (X /\ Y) by A12, XBOOLE_0:def 4;

        end;

        hence thesis by A4, A5, Th40;

      end;

        suppose

         A13: L is with_infima;

        let x,y be Element of L;

        assume that

         A14: x in (X /\ Y) and

         A15: y in (X /\ Y);

        

         A16: x in X by A14, XBOOLE_0:def 4;

        

         A17: x in Y by A14, XBOOLE_0:def 4;

        

         A18: y in X by A15, XBOOLE_0:def 4;

        

         A19: y in Y by A15, XBOOLE_0:def 4;

        consider zx be Element of L such that

         A20: zx in X and

         A21: x <= zx and

         A22: y <= zx by A2, A16, A18;

        consider zy be Element of L such that

         A23: zy in Y and

         A24: x <= zy and

         A25: y <= zy by A3, A17, A19;

        take z = (zx "/\" zy);

        

         A26: z <= zx by A13, YELLOW_0: 23;

        

         A27: z <= zy by A13, YELLOW_0: 23;

        

         A28: z in X by A2, A20, A26;

        z in Y by A3, A23, A27;

        hence z in (X /\ Y) by A28, XBOOLE_0:def 4;

        thus thesis by A13, A21, A22, A24, A25, YELLOW_0: 23;

      end;

    end;

    theorem :: WAYBEL_0:45

    for L be non empty antisymmetric RelStr st L is with_suprema or L is with_infima holds for X,Y be Subset of L st X is upper filtered & Y is upper filtered holds (X /\ Y) is filtered

    proof

      let L be non empty antisymmetric RelStr such that

       A1: L is with_suprema or L is with_infima;

      let X,Y be Subset of L such that

       A2: X is upper filtered and

       A3: Y is upper filtered;

      

       A4: (X /\ Y) is upper by A2, A3, Th29;

      per cases by A1;

        suppose

         A5: L is with_infima;

        now

          let x,y be Element of L;

          assume that

           A6: x in (X /\ Y) and

           A7: y in (X /\ Y);

          

           A8: x in X by A6, XBOOLE_0:def 4;

          

           A9: x in Y by A6, XBOOLE_0:def 4;

          

           A10: y in X by A7, XBOOLE_0:def 4;

          

           A11: y in Y by A7, XBOOLE_0:def 4;

          

           A12: (x "/\" y) in X by A2, A5, A8, A10, Th41;

          (x "/\" y) in Y by A3, A5, A9, A11, Th41;

          hence (x "/\" y) in (X /\ Y) by A12, XBOOLE_0:def 4;

        end;

        hence thesis by A4, A5, Th41;

      end;

        suppose

         A13: L is with_suprema;

        let x,y be Element of L;

        assume that

         A14: x in (X /\ Y) and

         A15: y in (X /\ Y);

        

         A16: x in X by A14, XBOOLE_0:def 4;

        

         A17: x in Y by A14, XBOOLE_0:def 4;

        

         A18: y in X by A15, XBOOLE_0:def 4;

        

         A19: y in Y by A15, XBOOLE_0:def 4;

        consider zx be Element of L such that

         A20: zx in X and

         A21: x >= zx and

         A22: y >= zx by A2, A16, A18;

        consider zy be Element of L such that

         A23: zy in Y and

         A24: x >= zy and

         A25: y >= zy by A3, A17, A19;

        take z = (zx "\/" zy);

        

         A26: z >= zx by A13, YELLOW_0: 22;

        

         A27: z >= zy by A13, YELLOW_0: 22;

        

         A28: z in X by A2, A20, A26;

        z in Y by A3, A23, A27;

        hence z in (X /\ Y) by A28, XBOOLE_0:def 4;

        thus thesis by A13, A21, A22, A24, A25, YELLOW_0: 22;

      end;

    end;

    theorem :: WAYBEL_0:46

    for L be RelStr, A be Subset-Family of L st (for X be Subset of L st X in A holds X is directed) & (for X,Y be Subset of L st X in A & Y in A holds ex Z be Subset of L st Z in A & (X \/ Y) c= Z) holds for X be Subset of L st X = ( union A) holds X is directed

    proof

      let L be RelStr, A be Subset-Family of L such that

       A1: for X be Subset of L st X in A holds X is directed and

       A2: for X,Y be Subset of L st X in A & Y in A holds ex Z be Subset of L st Z in A & (X \/ Y) c= Z;

      let Z be Subset of L;

      assume

       A3: Z = ( union A);

      let x,y be Element of L;

      assume x in Z;

      then

      consider X be set such that

       A4: x in X and

       A5: X in A by A3, TARSKI:def 4;

      assume y in Z;

      then

      consider Y be set such that

       A6: y in Y and

       A7: Y in A by A3, TARSKI:def 4;

      reconsider X, Y as Subset of L by A5, A7;

      consider W be Subset of L such that

       A8: W in A and

       A9: (X \/ Y) c= W by A2, A5, A7;

      

       A10: X c= (X \/ Y) by XBOOLE_1: 7;

      

       A11: Y c= (X \/ Y) by XBOOLE_1: 7;

      

       A12: x in (X \/ Y) by A4, A10;

      

       A13: y in (X \/ Y) by A6, A11;

      W is directed by A1, A8;

      then

      consider z be Element of L such that

       A14: z in W and

       A15: x <= z and

       A16: y <= z by A9, A12, A13;

      take z;

      thus thesis by A3, A8, A14, A15, A16, TARSKI:def 4;

    end;

    theorem :: WAYBEL_0:47

    for L be RelStr, A be Subset-Family of L st (for X be Subset of L st X in A holds X is filtered) & (for X,Y be Subset of L st X in A & Y in A holds ex Z be Subset of L st Z in A & (X \/ Y) c= Z) holds for X be Subset of L st X = ( union A) holds X is filtered

    proof

      let L be RelStr, A be Subset-Family of L such that

       A1: for X be Subset of L st X in A holds X is filtered and

       A2: for X,Y be Subset of L st X in A & Y in A holds ex Z be Subset of L st Z in A & (X \/ Y) c= Z;

      let Z be Subset of L;

      assume

       A3: Z = ( union A);

      let x,y be Element of L;

      assume x in Z;

      then

      consider X be set such that

       A4: x in X and

       A5: X in A by A3, TARSKI:def 4;

      assume y in Z;

      then

      consider Y be set such that

       A6: y in Y and

       A7: Y in A by A3, TARSKI:def 4;

      reconsider X, Y as Subset of L by A5, A7;

      consider W be Subset of L such that

       A8: W in A and

       A9: (X \/ Y) c= W by A2, A5, A7;

      

       A10: X c= (X \/ Y) by XBOOLE_1: 7;

      

       A11: Y c= (X \/ Y) by XBOOLE_1: 7;

      

       A12: x in (X \/ Y) by A4, A10;

      

       A13: y in (X \/ Y) by A6, A11;

      W is filtered by A1, A8;

      then

      consider z be Element of L such that

       A14: z in W and

       A15: x >= z and

       A16: y >= z by A9, A12, A13;

      take z;

      thus thesis by A3, A8, A14, A15, A16, TARSKI:def 4;

    end;

    definition

      let L be non empty reflexive transitive RelStr;

      let I be Ideal of L;

      :: WAYBEL_0:def21

      attr I is principal means ex x be Element of L st x in I & x is_>=_than I;

    end

    definition

      let L be non empty reflexive transitive RelStr;

      let F be Filter of L;

      :: WAYBEL_0:def22

      attr F is principal means ex x be Element of L st x in F & x is_<=_than F;

    end

    theorem :: WAYBEL_0:48

    for L be non empty reflexive transitive RelStr, I be Ideal of L holds I is principal iff ex x be Element of L st I = ( downarrow x)

    proof

      let L be non empty reflexive transitive RelStr, I be Ideal of L;

      thus I is principal implies ex x be Element of L st I = ( downarrow x)

      proof

        given x be Element of L such that

         A1: x in I and

         A2: x is_>=_than I;

        take x;

        thus I c= ( downarrow x) by A2, Th17;

        let z be object;

        assume

         A3: z in ( downarrow x);

        then

        reconsider z as Element of L;

        z <= x by A3, Th17;

        hence thesis by A1, Def19;

      end;

      given x be Element of L such that

       A4: I = ( downarrow x);

      take x;

      x <= x;

      hence x in I by A4, Th17;

      let y be Element of L;

      thus thesis by A4, Th17;

    end;

    theorem :: WAYBEL_0:49

    for L be non empty reflexive transitive RelStr, F be Filter of L holds F is principal iff ex x be Element of L st F = ( uparrow x)

    proof

      let L be non empty reflexive transitive RelStr, I be Filter of L;

      thus I is principal implies ex x be Element of L st I = ( uparrow x)

      proof

        given x be Element of L such that

         A1: x in I and

         A2: x is_<=_than I;

        take x;

        thus I c= ( uparrow x) by A2, Th18;

        let z be object;

        assume

         A3: z in ( uparrow x);

        then

        reconsider z as Element of L;

        z >= x by A3, Th18;

        hence thesis by A1, Def20;

      end;

      given x be Element of L such that

       A4: I = ( uparrow x);

      take x;

      x <= x;

      hence x in I by A4, Th18;

      let y be Element of L;

      thus thesis by A4, Th18;

    end;

    definition

      let L be non empty reflexive transitive RelStr;

      :: WAYBEL_0:def23

      func Ids L -> set equals the set of all X where X be Ideal of L;

      correctness ;

      :: WAYBEL_0:def24

      func Filt L -> set equals the set of all X where X be Filter of L;

      correctness ;

    end

    definition

      let L be non empty reflexive transitive RelStr;

      :: WAYBEL_0:def25

      func Ids_0 L -> set equals (( Ids L) \/ { {} });

      correctness ;

      :: WAYBEL_0:def26

      func Filt_0 L -> set equals (( Filt L) \/ { {} });

      correctness ;

    end

    definition

      let L be non empty RelStr;

      let X be Subset of L;

      set D = { ( "\/" (Y,L)) where Y be finite Subset of X : ex_sup_of (Y,L) };

      

       A1: D c= the carrier of L

      proof

        let x be object;

        assume x in D;

        then ex Y be finite Subset of X st x = ( "\/" (Y,L)) & ex_sup_of (Y,L);

        hence thesis;

      end;

      :: WAYBEL_0:def27

      func finsups X -> Subset of L equals { ( "\/" (Y,L)) where Y be finite Subset of X : ex_sup_of (Y,L) };

      correctness by A1;

      set D = { ( "/\" (Y,L)) where Y be finite Subset of X : ex_inf_of (Y,L) };

      

       A2: D c= the carrier of L

      proof

        let x be object;

        assume x in D;

        then ex Y be finite Subset of X st x = ( "/\" (Y,L)) & ex_inf_of (Y,L);

        hence thesis;

      end;

      :: WAYBEL_0:def28

      func fininfs X -> Subset of L equals { ( "/\" (Y,L)) where Y be finite Subset of X : ex_inf_of (Y,L) };

      correctness by A2;

    end

    registration

      let L be non empty antisymmetric lower-bounded RelStr;

      let X be Subset of L;

      cluster ( finsups X) -> non empty;

      coherence

      proof

         ex_sup_of ( {} ,L) by YELLOW_0: 42;

        then ( "\/" (( {} X),L)) in ( finsups X);

        hence thesis;

      end;

    end

    registration

      let L be non empty antisymmetric upper-bounded RelStr;

      let X be Subset of L;

      cluster ( fininfs X) -> non empty;

      coherence

      proof

         ex_inf_of ( {} ,L) by YELLOW_0: 43;

        then ( "/\" (( {} X),L)) in ( fininfs X);

        hence thesis;

      end;

    end

    registration

      let L be non empty reflexive antisymmetric RelStr;

      let X be non empty Subset of L;

      cluster ( finsups X) -> non empty;

      coherence

      proof

        set x = the Element of X;

        reconsider y = x as Element of L;

        reconsider Z = {y} as finite Subset of X by ZFMISC_1: 31;

         ex_sup_of (Z,L) by YELLOW_0: 38;

        then ( "\/" (Z,L)) in ( finsups X);

        hence thesis;

      end;

      cluster ( fininfs X) -> non empty;

      coherence

      proof

        set x = the Element of X;

        reconsider y = x as Element of L;

        reconsider Z = {y} as finite Subset of X by ZFMISC_1: 31;

         ex_inf_of (Z,L) by YELLOW_0: 38;

        then ( "/\" (Z,L)) in ( fininfs X);

        hence thesis;

      end;

    end

    theorem :: WAYBEL_0:50

    

     Th50: for L be non empty reflexive antisymmetric RelStr holds for X be Subset of L holds X c= ( finsups X) & X c= ( fininfs X)

    proof

      let L be non empty reflexive antisymmetric RelStr;

      let X be Subset of L;

      hereby

        let x be object;

        assume

         A1: x in X;

        then

        reconsider y = x as Element of L;

        reconsider Y = {x} as finite Subset of X by A1, ZFMISC_1: 31;

        

         A2: y = ( "\/" (Y,L)) by YELLOW_0: 39;

         ex_sup_of ( {y},L) by YELLOW_0: 38;

        hence x in ( finsups X) by A2;

      end;

      let x be object;

      assume

       A3: x in X;

      then

      reconsider y = x as Element of L;

      reconsider Y = {x} as finite Subset of X by A3, ZFMISC_1: 31;

      

       A4: y = ( "/\" (Y,L)) by YELLOW_0: 39;

       ex_inf_of ( {y},L) by YELLOW_0: 38;

      hence x in ( fininfs X) by A4;

    end;

    theorem :: WAYBEL_0:51

    

     Th51: for L be non empty transitive RelStr holds for X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F) holds F is directed

    proof

      let L be non empty transitive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F;

      let x,y be Element of L;

      assume

       A4: x in F;

      then

      consider Y1 be finite Subset of X such that

       A5: ex_sup_of (Y1,L) and

       A6: x = ( "\/" (Y1,L)) by A2;

      assume y in F;

      then

      consider Y2 be finite Subset of X such that

       A7: ex_sup_of (Y2,L) and

       A8: y = ( "\/" (Y2,L)) by A2;

      take z = ( "\/" ((Y1 \/ Y2),L));

      

       A9: Y1 = {} & Y2 = {} & ( {} \/ {} ) = {} or (Y1 \/ Y2) <> {} ;

      hence z in F by A3, A4, A6;

       ex_sup_of ((Y1 \/ Y2),L) by A1, A5, A9;

      hence thesis by A5, A6, A7, A8, XBOOLE_1: 7, YELLOW_0: 34;

    end;

    registration

      let L be with_suprema Poset;

      let X be Subset of L;

      cluster ( finsups X) -> directed;

      coherence

      proof

        reconsider X as Subset of L;

         A1:

        now

          let Y be finite Subset of X;

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

          hence Y <> {} implies ex_sup_of (Y,L) by YELLOW_0: 54;

        end;

         A2:

        now

          let x be Element of L;

          assume x in ( finsups X);

          then ex Y be finite Subset of X st x = ( "\/" (Y,L)) & ex_sup_of (Y,L);

          hence ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L));

        end;

        now

          let Y be finite Subset of X;

          reconsider Z = Y as Subset of L by XBOOLE_1: 1;

          assume Y <> {} ;

          then ex_sup_of (Z,L) by YELLOW_0: 54;

          hence ( "\/" (Y,L)) in ( finsups X);

        end;

        hence thesis by A1, A2, Th51;

      end;

    end

    theorem :: WAYBEL_0:52

    

     Th52: for L be non empty transitive reflexive RelStr, X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F) holds for x be Element of L holds x is_>=_than X iff x is_>=_than F

    proof

      let L be non empty transitive reflexive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F;

      let x be Element of L;

      thus x is_>=_than X implies x is_>=_than F

      proof

        assume

         A4: x is_>=_than X;

        let y be Element of L;

        assume y in F;

        then

        consider Y be finite Subset of X such that

         A5: ex_sup_of (Y,L) and

         A6: y = ( "\/" (Y,L)) by A2;

        x is_>=_than Y by A4;

        hence thesis by A5, A6, YELLOW_0:def 9;

      end;

      assume

       A7: x is_>=_than F;

      let y be Element of L;

      assume y in X;

      then

       A8: {y} c= X by ZFMISC_1: 31;

      then

       A9: ( sup {y}) in F by A3;

       ex_sup_of ( {y},L) by A1, A8;

      then

       A10: {y} is_<=_than ( sup {y}) by YELLOW_0:def 9;

      

       A11: ( sup {y}) <= x by A7, A9;

      y <= ( sup {y}) by A10, YELLOW_0: 7;

      hence thesis by A11, ORDERS_2: 3;

    end;

    theorem :: WAYBEL_0:53

    

     Th53: for L be non empty transitive reflexive RelStr, X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F) holds ex_sup_of (X,L) iff ex_sup_of (F,L)

    proof

      let L be non empty transitive reflexive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F;

      for x be Element of L holds x is_>=_than X iff x is_>=_than F by A1, A2, A3, Th52;

      hence thesis by YELLOW_0: 46;

    end;

    theorem :: WAYBEL_0:54

    

     Th54: for L be non empty transitive reflexive RelStr, X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F) & ex_sup_of (X,L) holds ( sup F) = ( sup X)

    proof

      let L be non empty transitive reflexive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_sup_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "\/" (Y,L)) in F;

      for x be Element of L holds x is_>=_than X iff x is_>=_than F by A1, A2, A3, Th52;

      hence thesis by YELLOW_0: 47;

    end;

    theorem :: WAYBEL_0:55

    for L be with_suprema Poset, X be Subset of L st ex_sup_of (X,L) or L is complete holds ( sup X) = ( sup ( finsups X))

    proof

      let L be with_suprema Poset, X be Subset of L;

      assume ex_sup_of (X,L) or L is complete;

      then

       A1: ex_sup_of (X,L) by YELLOW_0: 17;

       A2:

      now

        let Y be finite Subset of X;

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

        hence Y <> {} implies ex_sup_of (Y,L) by YELLOW_0: 54;

      end;

       A3:

      now

        let x be Element of L;

        assume x in ( finsups X);

        then ex Y be finite Subset of X st x = ( "\/" (Y,L)) & ex_sup_of (Y,L);

        hence ex Y be finite Subset of X st ex_sup_of (Y,L) & x = ( "\/" (Y,L));

      end;

      now

        let Y be finite Subset of X;

        reconsider Z = Y as Subset of L by XBOOLE_1: 1;

        assume Y <> {} ;

        then ex_sup_of (Z,L) by YELLOW_0: 54;

        hence ( "\/" (Y,L)) in ( finsups X);

      end;

      hence thesis by A1, A2, A3, Th54;

    end;

    theorem :: WAYBEL_0:56

    

     Th56: for L be non empty transitive RelStr holds for X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F) holds F is filtered

    proof

      let L be non empty transitive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F;

      let x,y be Element of L;

      assume

       A4: x in F;

      then

      consider Y1 be finite Subset of X such that

       A5: ex_inf_of (Y1,L) and

       A6: x = ( "/\" (Y1,L)) by A2;

      assume y in F;

      then

      consider Y2 be finite Subset of X such that

       A7: ex_inf_of (Y2,L) and

       A8: y = ( "/\" (Y2,L)) by A2;

      take z = ( "/\" ((Y1 \/ Y2),L));

      

       A9: Y1 = {} & Y2 = {} & ( {} \/ {} ) = {} or (Y1 \/ Y2) <> {} ;

      hence z in F by A3, A4, A6;

       ex_inf_of ((Y1 \/ Y2),L) by A1, A5, A9;

      hence thesis by A5, A6, A7, A8, XBOOLE_1: 7, YELLOW_0: 35;

    end;

    registration

      let L be with_infima Poset;

      let X be Subset of L;

      cluster ( fininfs X) -> filtered;

      coherence

      proof

        reconsider X as Subset of L;

         A1:

        now

          let Y be finite Subset of X;

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

          hence Y <> {} implies ex_inf_of (Y,L) by YELLOW_0: 55;

        end;

         A2:

        now

          let x be Element of L;

          assume x in ( fininfs X);

          then ex Y be finite Subset of X st x = ( "/\" (Y,L)) & ex_inf_of (Y,L);

          hence ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L));

        end;

        now

          let Y be finite Subset of X;

          reconsider Z = Y as Subset of L by XBOOLE_1: 1;

          assume Y <> {} ;

          then ex_inf_of (Z,L) by YELLOW_0: 55;

          hence ( "/\" (Y,L)) in ( fininfs X);

        end;

        hence thesis by A1, A2, Th56;

      end;

    end

    theorem :: WAYBEL_0:57

    

     Th57: for L be non empty transitive reflexive RelStr, X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F) holds for x be Element of L holds x is_<=_than X iff x is_<=_than F

    proof

      let L be non empty transitive reflexive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F;

      let x be Element of L;

      thus x is_<=_than X implies x is_<=_than F

      proof

        assume

         A4: x is_<=_than X;

        let y be Element of L;

        assume y in F;

        then

        consider Y be finite Subset of X such that

         A5: ex_inf_of (Y,L) and

         A6: y = ( "/\" (Y,L)) by A2;

        x is_<=_than Y by A4;

        hence x <= y by A5, A6, YELLOW_0:def 10;

      end;

      assume

       A7: x is_<=_than F;

      let y be Element of L;

      assume y in X;

      then

       A8: {y} c= X by ZFMISC_1: 31;

      then

       A9: ( inf {y}) in F by A3;

       ex_inf_of ( {y},L) by A1, A8;

      then

       A10: {y} is_>=_than ( inf {y}) by YELLOW_0:def 10;

      

       A11: ( inf {y}) >= x by A7, A9;

      y >= ( inf {y}) by A10, YELLOW_0: 7;

      hence thesis by A11, ORDERS_2: 3;

    end;

    theorem :: WAYBEL_0:58

    

     Th58: for L be non empty transitive reflexive RelStr, X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F) holds ex_inf_of (X,L) iff ex_inf_of (F,L)

    proof

      let L be non empty transitive reflexive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F;

      for x be Element of L holds x is_<=_than X iff x is_<=_than F by A1, A2, A3, Th57;

      hence thesis by YELLOW_0: 48;

    end;

    theorem :: WAYBEL_0:59

    

     Th59: for L be non empty transitive reflexive RelStr, X,F be Subset of L st (for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L)) & (for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L))) & (for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F) & ex_inf_of (X,L) holds ( inf F) = ( inf X)

    proof

      let L be non empty transitive reflexive RelStr;

      let X,F be Subset of L such that

       A1: for Y be finite Subset of X st Y <> {} holds ex_inf_of (Y,L) and

       A2: for x be Element of L st x in F holds ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L)) and

       A3: for Y be finite Subset of X st Y <> {} holds ( "/\" (Y,L)) in F;

      for x be Element of L holds x is_<=_than X iff x is_<=_than F by A1, A2, A3, Th57;

      hence thesis by YELLOW_0: 49;

    end;

    theorem :: WAYBEL_0:60

    for L be with_infima Poset, X be Subset of L st ex_inf_of (X,L) or L is complete holds ( inf X) = ( inf ( fininfs X))

    proof

      let L be with_infima Poset, X be Subset of L;

      assume ex_inf_of (X,L) or L is complete;

      then

       A1: ex_inf_of (X,L) by YELLOW_0: 17;

       A2:

      now

        let Y be finite Subset of X;

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

        hence Y <> {} implies ex_inf_of (Y,L) by YELLOW_0: 55;

      end;

       A3:

      now

        let x be Element of L;

        assume x in ( fininfs X);

        then ex Y be finite Subset of X st x = ( "/\" (Y,L)) & ex_inf_of (Y,L);

        hence ex Y be finite Subset of X st ex_inf_of (Y,L) & x = ( "/\" (Y,L));

      end;

      now

        let Y be finite Subset of X;

        reconsider Z = Y as Subset of L by XBOOLE_1: 1;

        assume Y <> {} ;

        then ex_inf_of (Z,L) by YELLOW_0: 55;

        hence ( "/\" (Y,L)) in ( fininfs X);

      end;

      hence thesis by A1, A2, A3, Th59;

    end;

    theorem :: WAYBEL_0:61

    for L be with_suprema Poset, X be Subset of L holds X c= ( downarrow ( finsups X)) & for I be Ideal of L st X c= I holds ( downarrow ( finsups X)) c= I

    proof

      let L be with_suprema Poset, X be Subset of L;

      

       A1: X c= ( finsups X) by Th50;

      ( finsups X) c= ( downarrow ( finsups X)) by Th16;

      hence X c= ( downarrow ( finsups X)) by A1;

      let I be Ideal of L such that

       A2: X c= I;

      let x be object;

      assume

       A3: x in ( downarrow ( finsups X));

      then

      reconsider x as Element of L;

      consider y be Element of L such that

       A4: x <= y and

       A5: y in ( finsups X) by A3, Def15;

      consider Y be finite Subset of X such that

       A6: y = ( "\/" (Y,L)) and

       A7: ex_sup_of (Y,L) by A5;

      set i = the Element of I;

      reconsider i as Element of L;

      

       A8: ex_sup_of ( {i},L) by YELLOW_0: 38;

      

       A9: ( sup {i}) = i by YELLOW_0: 39;

       A10:

      now

        assume ex_sup_of ( {} ,L);

        then ( "\/" ( {} ,L)) <= ( sup {i}) by A8, XBOOLE_1: 2, YELLOW_0: 34;

        hence ( "\/" ( {} ,L)) in I by A9, Def19;

      end;

      Y c= I by A2;

      then y in I by A6, A7, A10, Th42;

      hence thesis by A4, Def19;

    end;

    theorem :: WAYBEL_0:62

    for L be with_infima Poset, X be Subset of L holds X c= ( uparrow ( fininfs X)) & for F be Filter of L st X c= F holds ( uparrow ( fininfs X)) c= F

    proof

      let L be with_infima Poset, X be Subset of L;

      

       A1: X c= ( fininfs X) by Th50;

      ( fininfs X) c= ( uparrow ( fininfs X)) by Th16;

      hence X c= ( uparrow ( fininfs X)) by A1;

      let I be Filter of L such that

       A2: X c= I;

      let x be object;

      assume

       A3: x in ( uparrow ( fininfs X));

      then

      reconsider x as Element of L;

      consider y be Element of L such that

       A4: x >= y and

       A5: y in ( fininfs X) by A3, Def16;

      consider Y be finite Subset of X such that

       A6: y = ( "/\" (Y,L)) and

       A7: ex_inf_of (Y,L) by A5;

      set i = the Element of I;

      reconsider i as Element of L;

      

       A8: ex_inf_of ( {i},L) by YELLOW_0: 38;

      

       A9: ( inf {i}) = i by YELLOW_0: 39;

       A10:

      now

        assume ex_inf_of ( {} ,L);

        then ( "/\" ( {} ,L)) >= ( inf {i}) by A8, XBOOLE_1: 2, YELLOW_0: 35;

        hence ( "/\" ( {} ,L)) in I by A9, Def20;

      end;

      Y c= I by A2;

      then y in I by A6, A7, A10, Th43;

      hence thesis by A4, Def20;

    end;

    begin

    definition

      let L be non empty RelStr;

      :: WAYBEL_0:def29

      attr L is connected means

      : Def29: for x,y be Element of L holds x <= y or y <= x;

    end

    registration

      cluster trivial -> connected for non empty reflexive RelStr;

      coherence

      proof

        let L be non empty reflexive RelStr;

        assume

         A1: for x,y be Element of L holds x = y;

        let z1,z2 be Element of L;

        z1 = z2 by A1;

        hence thesis by ORDERS_2: 1;

      end;

    end

    registration

      cluster connected for non empty Poset;

      existence

      proof

        set O = the Order of { 0 };

        take L = RelStr (# { 0 }, O #);

        let x,y be Element of L;

        

         A1: x = 0 by TARSKI:def 1;

        y = 0 by TARSKI:def 1;

        hence thesis by A1, ORDERS_2: 1;

      end;

    end

    definition

      mode Chain is connected non empty Poset;

    end

    registration

      let L be Chain;

      cluster (L ~ ) -> connected;

      coherence

      proof

        let x,y be Element of (L ~ );

        

         A1: (( ~ x) ~ ) = ( ~ x);

        

         A2: (( ~ y) ~ ) = ( ~ y);

        ( ~ x) <= ( ~ y) or ( ~ x) >= ( ~ y) by Def29;

        hence thesis by A1, A2, LATTICE3: 9;

      end;

    end

    begin

    definition

      mode Semilattice is with_infima Poset;

      mode sup-Semilattice is with_suprema Poset;

      mode LATTICE is with_infima with_suprema Poset;

    end

    theorem :: WAYBEL_0:63

    for L be Semilattice holds for X be upper non empty Subset of L holds X is Filter of L iff ( subrelstr X) is meet-inheriting

    proof

      let L be Semilattice, X be upper non empty Subset of L;

      set S = ( subrelstr X);

      

       A1: the carrier of S = X by YELLOW_0:def 15;

      hereby

        assume

         A2: X is Filter of L;

        thus S is meet-inheriting

        proof

          let x,y be Element of L;

          assume that

           A3: x in the carrier of S and

           A4: y in the carrier of S and

           A5: ex_inf_of ( {x, y},L);

          consider z be Element of L such that

           A6: z in X and

           A7: x >= z and

           A8: y >= z by A1, A2, A3, A4, Def2;

          z is_<=_than {x, y} by A7, A8, YELLOW_0: 8;

          then z <= ( inf {x, y}) by A5, YELLOW_0:def 10;

          hence thesis by A1, A6, Def20;

        end;

      end;

      assume

       A9: for x,y be Element of L st x in the carrier of S & y in the carrier of S & ex_inf_of ( {x, y},L) holds ( inf {x, y}) in the carrier of S;

      X is filtered

      proof

        let x,y be Element of L;

        assume that

         A10: x in X and

         A11: y in X;

        take z = ( inf {x, y});

        

         A12: z = (x "/\" y) by YELLOW_0: 40;

         ex_inf_of ( {x, y},L) by YELLOW_0: 21;

        hence z in X & z <= x & z <= y by A1, A9, A10, A11, A12, YELLOW_0: 19;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL_0:64

    for L be sup-Semilattice holds for X be lower non empty Subset of L holds X is Ideal of L iff ( subrelstr X) is join-inheriting

    proof

      let L be sup-Semilattice, X be lower non empty Subset of L;

      set S = ( subrelstr X);

      

       A1: the carrier of S = X by YELLOW_0:def 15;

      hereby

        assume

         A2: X is Ideal of L;

        thus S is join-inheriting

        proof

          let x,y be Element of L;

          assume that

           A3: x in the carrier of S and

           A4: y in the carrier of S and

           A5: ex_sup_of ( {x, y},L);

          consider z be Element of L such that

           A6: z in X and

           A7: x <= z and

           A8: y <= z by A1, A2, A3, A4, Def1;

          z is_>=_than {x, y} by A7, A8, YELLOW_0: 8;

          then z >= ( sup {x, y}) by A5, YELLOW_0:def 9;

          hence thesis by A1, A6, Def19;

        end;

      end;

      assume

       A9: for x,y be Element of L st x in the carrier of S & y in the carrier of S & ex_sup_of ( {x, y},L) holds ( sup {x, y}) in the carrier of S;

      X is directed

      proof

        let x,y be Element of L;

        assume that

         A10: x in X and

         A11: y in X;

        take z = ( sup {x, y});

        

         A12: z = (x "\/" y) by YELLOW_0: 41;

         ex_sup_of ( {x, y},L) by YELLOW_0: 20;

        hence z in X & x <= z & y <= z by A1, A9, A10, A11, A12, YELLOW_0: 18;

      end;

      hence thesis;

    end;

    begin

    definition

      let S,T be non empty RelStr;

      let f be Function of S, T;

      let X be Subset of S;

      :: WAYBEL_0:def30

      pred f preserves_inf_of X means ex_inf_of (X,S) implies ex_inf_of ((f .: X),T) & ( inf (f .: X)) = (f . ( inf X));

      :: WAYBEL_0:def31

      pred f preserves_sup_of X means ex_sup_of (X,S) implies ex_sup_of ((f .: X),T) & ( sup (f .: X)) = (f . ( sup X));

    end

    theorem :: WAYBEL_0:65

    for S1,S2,T1,T2 be non empty RelStr st the RelStr of S1 = the RelStr of T1 & the RelStr of S2 = the RelStr of T2 holds for f be Function of S1, S2, g be Function of T1, T2 st f = g holds for X be Subset of S1, Y be Subset of T1 st X = Y holds (f preserves_sup_of X implies g preserves_sup_of Y) & (f preserves_inf_of X implies g preserves_inf_of Y)

    proof

      let S1,S2,T1,T2 be non empty RelStr such that

       A1: the RelStr of S1 = the RelStr of T1 and

       A2: the RelStr of S2 = the RelStr of T2;

      let f be Function of S1, S2, g be Function of T1, T2 such that

       A3: f = g;

      let X be Subset of S1, Y be Subset of T1 such that

       A4: X = Y;

      thus f preserves_sup_of X implies g preserves_sup_of Y

      proof

        assume

         A5: ex_sup_of (X,S1) implies ex_sup_of ((f .: X),S2) & ( sup (f .: X)) = (f . ( sup X));

        assume

         A6: ex_sup_of (Y,T1);

        hence ex_sup_of ((g .: Y),T2) by A1, A2, A3, A4, A5, YELLOW_0: 14;

        ( sup (f .: X)) = ( sup (g .: Y)) by A1, A2, A3, A4, A5, A6, YELLOW_0: 14, YELLOW_0: 26;

        hence thesis by A1, A3, A4, A5, A6, YELLOW_0: 14, YELLOW_0: 26;

      end;

      assume

       A7: ex_inf_of (X,S1) implies ex_inf_of ((f .: X),S2) & ( inf (f .: X)) = (f . ( inf X));

      assume

       A8: ex_inf_of (Y,T1);

      hence ex_inf_of ((g .: Y),T2) by A1, A2, A3, A4, A7, YELLOW_0: 14;

      ( inf (f .: X)) = ( inf (g .: Y)) by A1, A2, A3, A4, A7, A8, YELLOW_0: 14, YELLOW_0: 27;

      hence thesis by A1, A3, A4, A7, A8, YELLOW_0: 14, YELLOW_0: 27;

    end;

    definition

      let L1,L2 be non empty RelStr;

      let f be Function of L1, L2;

      :: WAYBEL_0:def32

      attr f is infs-preserving means for X be Subset of L1 holds f preserves_inf_of X;

      :: WAYBEL_0:def33

      attr f is sups-preserving means for X be Subset of L1 holds f preserves_sup_of X;

      :: WAYBEL_0:def34

      attr f is meet-preserving means for x,y be Element of L1 holds f preserves_inf_of {x, y};

      :: WAYBEL_0:def35

      attr f is join-preserving means for x,y be Element of L1 holds f preserves_sup_of {x, y};

      :: WAYBEL_0:def36

      attr f is filtered-infs-preserving means for X be Subset of L1 st X is non empty filtered holds f preserves_inf_of X;

      :: WAYBEL_0:def37

      attr f is directed-sups-preserving means for X be Subset of L1 st X is non empty directed holds f preserves_sup_of X;

    end

    registration

      let L1,L2 be non empty RelStr;

      cluster infs-preserving -> filtered-infs-preserving meet-preserving for Function of L1, L2;

      coherence ;

      cluster sups-preserving -> directed-sups-preserving join-preserving for Function of L1, L2;

      coherence ;

    end

    definition

      let S,T be RelStr;

      let f be Function of S, T;

      :: WAYBEL_0:def38

      attr f is isomorphic means

      : Def38: f is one-to-one monotone & ex g be Function of T, S st g = (f " ) & g is monotone if S is non empty & T is non empty

      otherwise S is empty & T is empty;

      correctness ;

    end

    theorem :: WAYBEL_0:66

    

     Th66: for S,T be non empty RelStr, f be Function of S, T holds f is isomorphic iff f is one-to-one & ( rng f) = the carrier of T & for x,y be Element of S holds x <= y iff (f . x) <= (f . y)

    proof

      let S,T be non empty RelStr;

      let f be Function of S, T;

      hereby

        assume

         A1: f is isomorphic;

        hence f is one-to-one by Def38;

        consider g be Function of T, S such that

         A2: g = (f " ) and

         A3: g is monotone by A1, Def38;

        

         A4: f is one-to-one monotone by A1, Def38;

        then ( rng f) = ( dom g) by A2, FUNCT_1: 33;

        hence ( rng f) = the carrier of T by FUNCT_2:def 1;

        let x,y be Element of S;

        thus x <= y implies (f . x) <= (f . y) by A4;

        assume

         A5: (f . x) <= (f . y);

        

         A6: (g . (f . x)) = x by A2, A4, FUNCT_2: 26;

        (g . (f . y)) = y by A2, A4, FUNCT_2: 26;

        hence x <= y by A3, A5, A6;

      end;

      assume that

       A7: f is one-to-one and

       A8: ( rng f) = the carrier of T and

       A9: for x,y be Element of S holds x <= y iff (f . x) <= (f . y);

      per cases ;

        case S is non empty & T is non empty;

        thus f is one-to-one by A7;

        thus for x,y be Element of S st x <= y holds for a,b be Element of T st a = (f . x) & b = (f . y) holds a <= b by A9;

        reconsider g = (f " ) as Function of T, S by A7, A8, FUNCT_2: 25;

        take g;

        thus g = (f " );

        let x,y be Element of T;

        consider a be object such that

         A10: a in ( dom f) and

         A11: x = (f . a) by A8, FUNCT_1:def 3;

        consider b be object such that

         A12: b in ( dom f) and

         A13: y = (f . b) by A8, FUNCT_1:def 3;

        reconsider a, b as Element of S by A10, A12;

        

         A14: (g . x) = a by A7, A11, FUNCT_2: 26;

        (g . y) = b by A7, A13, FUNCT_2: 26;

        hence thesis by A9, A11, A13, A14;

      end;

        case S is empty or T is empty;

        hence thesis;

      end;

    end;

    registration

      let S,T be non empty RelStr;

      cluster isomorphic -> one-to-one monotone for Function of S, T;

      coherence by Def38;

    end

    theorem :: WAYBEL_0:67

    for S,T be non empty RelStr, f be Function of S, T st f is isomorphic holds (f " ) is Function of T, S & ( rng (f " )) = the carrier of S

    proof

      let S,T be non empty RelStr, f be Function of S, T;

      assume

       A1: f is isomorphic;

      then

       A2: ( rng f) = the carrier of T by Th66;

      

       A3: ( dom f) = the carrier of S by FUNCT_2:def 1;

      

       A4: ( dom (f " )) = the carrier of T by A1, A2, FUNCT_1: 33;

      ( rng (f " )) = the carrier of S by A1, A3, FUNCT_1: 33;

      hence thesis by A4, FUNCT_2: 1;

    end;

    theorem :: WAYBEL_0:68

    for S,T be non empty RelStr, f be Function of S, T st f is isomorphic holds for g be Function of T, S st g = (f " ) holds g is isomorphic

    proof

      let S,T be non empty RelStr, f be Function of S, T;

      assume

       A1: f is isomorphic;

      then

       A2: ex h be Function of T, S st (h = (f " )) & (h is monotone) by Def38;

      let g be Function of T, S;

      assume

       A3: g = (f " );

      per cases ;

        case T is non empty & S is non empty;

        thus g is one-to-one monotone by A1, A2, A3, FUNCT_1: 40;

        ((f " ) " ) = f by A1, FUNCT_1: 43;

        hence thesis by A1, A3;

      end;

        case T is empty or S is empty;

        hence thesis;

      end;

    end;

    theorem :: WAYBEL_0:69

    

     Th69: for S,T be non empty Poset, f be Function of S, T st for X be Filter of S holds f preserves_inf_of X holds f is monotone

    proof

      let S,T be non empty Poset, f be Function of S, T;

      assume

       A1: for X be Filter of S holds f preserves_inf_of X;

      let x,y be Element of S;

      

       A2: ex_inf_of ( {x},S) by YELLOW_0: 38;

      

       A3: ex_inf_of ( {y},S) by YELLOW_0: 38;

      

       A4: f preserves_inf_of ( uparrow x) by A1;

      

       A5: f preserves_inf_of ( uparrow y) by A1;

      

       A6: ex_inf_of (( uparrow x),S) by A2, Th37;

      

       A7: ex_inf_of (( uparrow y),S) by A3, Th37;

      

       A8: ex_inf_of ((f .: ( uparrow x)),T) by A4, A6;

      

       A9: ex_inf_of ((f .: ( uparrow y)),T) by A5, A7;

      

       A10: ( inf (f .: ( uparrow x))) = (f . ( inf ( uparrow x))) by A4, A6;

      

       A11: ( inf (f .: ( uparrow y))) = (f . ( inf ( uparrow y))) by A5, A7;

      assume x <= y;

      then

       A12: ( uparrow y) c= ( uparrow x) by Th22;

      

       A13: ( inf (f .: ( uparrow x))) = (f . ( inf {x})) by A10, Th38, YELLOW_0: 38;

      

       A14: ( inf (f .: ( uparrow y))) = (f . ( inf {y})) by A11, Th38, YELLOW_0: 38;

      

       A15: ( inf (f .: ( uparrow x))) = (f . x) by A13, YELLOW_0: 39;

      ( inf (f .: ( uparrow y))) = (f . y) by A14, YELLOW_0: 39;

      hence thesis by A8, A9, A12, A15, RELAT_1: 123, YELLOW_0: 35;

    end;

    theorem :: WAYBEL_0:70

    for S,T be non empty Poset, f be Function of S, T st for X be Filter of S holds f preserves_inf_of X holds f is filtered-infs-preserving

    proof

      let S,T be non empty Poset, f be Function of S, T such that

       A1: for X be Filter of S holds f preserves_inf_of X;

      let X be Subset of S such that

       A2: X is non empty filtered and

       A3: ex_inf_of (X,S);

      reconsider Y = X as non empty filtered Subset of S by A2;

      ( uparrow Y) is Filter of S;

      then

       A4: f preserves_inf_of ( uparrow X) by A1;

      

       A5: ex_inf_of (( uparrow X),S) by A3, Th37;

      then

       A6: ex_inf_of ((f .: ( uparrow X)),T) by A4;

      

       A7: ( inf (f .: ( uparrow X))) = (f . ( inf ( uparrow X))) by A4, A5;

      

       A8: ( inf ( uparrow X)) = ( inf X) by A3, Th38;

      

       A9: (f .: X) c= (f .: ( uparrow X)) by Th16, RELAT_1: 123;

      

       A10: (f .: ( uparrow X)) is_>=_than (f . ( inf X)) by A6, A7, A8, YELLOW_0: 31;

      

       A11: (f .: X) is_>=_than (f . ( inf X)) by A9, A10;

       A12:

      now

        let b be Element of T;

        assume

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

        (f .: ( uparrow X)) is_>=_than b

        proof

          let a be Element of T;

          assume a in (f .: ( uparrow X));

          then

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

           A14: x in ( uparrow X) and

           A15: a = (f . x) by FUNCT_1:def 6;

          ( uparrow X) = { z where z be Element of S : ex y be Element of S st z >= y & y in X } by Th15;

          then

          consider z be Element of S such that

           A16: x = z and

           A17: ex y be Element of S st z >= y & y in X by A14;

          consider y be Element of S such that

           A18: z >= y and

           A19: y in X by A17;

          

           A20: f is monotone by A1, Th69;

          

           A21: (f . y) in (f .: X) by A19, FUNCT_2: 35;

          

           A22: (f . z) >= (f . y) by A18, A20;

          (f . y) >= b by A13, A21;

          hence thesis by A15, A16, A22, ORDERS_2: 3;

        end;

        hence (f . ( inf X)) >= b by A6, A7, A8, YELLOW_0: 31;

      end;

      hence ex_inf_of ((f .: X),T) by A11, YELLOW_0: 16;

      hence thesis by A11, A12, YELLOW_0:def 10;

    end;

    theorem :: WAYBEL_0:71

    for S be Semilattice, T be non empty Poset, f be Function of S, T st (for X be finite Subset of S holds f preserves_inf_of X) & (for X be non empty filtered Subset of S holds f preserves_inf_of X) holds f is infs-preserving

    proof

      let S be Semilattice, T be non empty Poset, f be Function of S, T such that

       A1: for X be finite Subset of S holds f preserves_inf_of X and

       A2: for X be non empty filtered Subset of S holds f preserves_inf_of X;

      let X be Subset of S such that

       A3: ex_inf_of (X,S);

      defpred P[ object] means ex Y be finite Subset of X st ex_inf_of (Y,S) & $1 = ( "/\" (Y,S));

      consider Z be set such that

       A4: for x be object holds x in Z iff x in the carrier of S & P[x] from XBOOLE_0:sch 1;

      Z c= the carrier of S by A4;

      then

      reconsider Z as Subset of S;

       A5:

      now

        let Y be finite Subset of X;

        Y is Subset of S by XBOOLE_1: 1;

        hence Y <> {} implies ex_inf_of (Y,S) by YELLOW_0: 55;

      end;

       A6:

      now

        let Y be finite Subset of X;

        reconsider Y9 = Y as Subset of S by XBOOLE_1: 1;

        assume Y <> {} ;

        then ex_inf_of (Y9,S) by YELLOW_0: 55;

        hence ( "/\" (Y,S)) in Z by A4;

      end;

      

       A7: for x be Element of S st x in Z holds ex Y be finite Subset of X st ex_inf_of (Y,S) & x = ( "/\" (Y,S)) by A4;

      then

       A8: Z is filtered by A5, A6, Th56;

      

       A9: ex_inf_of (Z,S) by A3, A5, A6, A7, Th58;

      Z = {} or Z <> {} ;

      then

       A10: f preserves_inf_of Z by A1, A2, A8;

      then

       A11: ex_inf_of ((f .: Z),T) by A9;

      

       A12: ( inf (f .: Z)) = (f . ( inf Z)) by A9, A10;

      

       A13: ( inf Z) = ( inf X) by A3, A5, A6, A7, Th59;

      X c= Z

      proof

        let x be object;

        assume

         A14: x in X;

        then

        reconsider Y = {x} as finite Subset of X by ZFMISC_1: 31;

        reconsider x as Element of S by A14;

        Y is Subset of S by XBOOLE_1: 1;

        then

         A15: ex_inf_of (Y,S) by YELLOW_0: 55;

        x = ( "/\" (Y,S)) by YELLOW_0: 39;

        hence thesis by A4, A15;

      end;

      then

       A16: (f .: X) c= (f .: Z) by RELAT_1: 123;

      

       A17: (f .: Z) is_>=_than (f . ( inf X)) by A11, A12, A13, YELLOW_0: 31;

      

       A18: (f .: X) is_>=_than (f . ( inf X)) by A16, A17;

       A19:

      now

        let b be Element of T;

        assume

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

        (f .: Z) is_>=_than b

        proof

          let a be Element of T;

          assume a in (f .: Z);

          then

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

           A21: x in Z and

           A22: a = (f . x) by FUNCT_1:def 6;

          consider Y be finite Subset of X such that

           A23: ex_inf_of (Y,S) and

           A24: x = ( "/\" (Y,S)) by A4, A21;

          reconsider Y as Subset of S by XBOOLE_1: 1;

          

           A25: (f .: Y) c= (f .: X) by RELAT_1: 123;

          

           A26: f preserves_inf_of Y by A1;

          

           A27: b is_<=_than (f .: Y) by A20, A25;

          

           A28: a = ( "/\" ((f .: Y),T)) by A22, A23, A24, A26;

           ex_inf_of ((f .: Y),T) by A23, A26;

          hence thesis by A27, A28, YELLOW_0:def 10;

        end;

        hence (f . ( inf X)) >= b by A11, A12, A13, YELLOW_0: 31;

      end;

      hence ex_inf_of ((f .: X),T) by A18, YELLOW_0: 16;

      hence thesis by A18, A19, YELLOW_0:def 10;

    end;

    theorem :: WAYBEL_0:72

    

     Th72: for S,T be non empty Poset, f be Function of S, T st for X be Ideal of S holds f preserves_sup_of X holds f is monotone

    proof

      let S,T be non empty Poset, f be Function of S, T;

      assume

       A1: for X be Ideal of S holds f preserves_sup_of X;

      let x,y be Element of S;

      

       A2: ex_sup_of ( {x},S) by YELLOW_0: 38;

      

       A3: ex_sup_of ( {y},S) by YELLOW_0: 38;

      

       A4: f preserves_sup_of ( downarrow x) by A1;

      

       A5: f preserves_sup_of ( downarrow y) by A1;

      

       A6: ex_sup_of (( downarrow x),S) by A2, Th32;

      

       A7: ex_sup_of (( downarrow y),S) by A3, Th32;

      

       A8: ex_sup_of ((f .: ( downarrow x)),T) by A4, A6;

      

       A9: ex_sup_of ((f .: ( downarrow y)),T) by A5, A7;

      

       A10: ( sup (f .: ( downarrow x))) = (f . ( sup ( downarrow x))) by A4, A6;

      

       A11: ( sup (f .: ( downarrow y))) = (f . ( sup ( downarrow y))) by A5, A7;

      assume x <= y;

      then

       A12: ( downarrow x) c= ( downarrow y) by Th21;

      

       A13: ( sup (f .: ( downarrow x))) = (f . ( sup {x})) by A10, Th33, YELLOW_0: 38;

      

       A14: ( sup (f .: ( downarrow y))) = (f . ( sup {y})) by A11, Th33, YELLOW_0: 38;

      

       A15: ( sup (f .: ( downarrow x))) = (f . x) by A13, YELLOW_0: 39;

      ( sup (f .: ( downarrow y))) = (f . y) by A14, YELLOW_0: 39;

      hence thesis by A8, A9, A12, A15, RELAT_1: 123, YELLOW_0: 34;

    end;

    theorem :: WAYBEL_0:73

    for S,T be non empty Poset, f be Function of S, T st for X be Ideal of S holds f preserves_sup_of X holds f is directed-sups-preserving

    proof

      let S,T be non empty Poset, f be Function of S, T such that

       A1: for X be Ideal of S holds f preserves_sup_of X;

      let X be Subset of S such that

       A2: X is non empty directed and

       A3: ex_sup_of (X,S);

      reconsider Y = X as non empty directed Subset of S by A2;

      ( downarrow Y) is Ideal of S;

      then

       A4: f preserves_sup_of ( downarrow X) by A1;

      

       A5: ex_sup_of (( downarrow X),S) by A3, Th32;

      then

       A6: ex_sup_of ((f .: ( downarrow X)),T) by A4;

      

       A7: ( sup (f .: ( downarrow X))) = (f . ( sup ( downarrow X))) by A4, A5;

      

       A8: ( sup ( downarrow X)) = ( sup X) by A3, Th33;

      

       A9: (f .: X) c= (f .: ( downarrow X)) by Th16, RELAT_1: 123;

      

       A10: (f .: ( downarrow X)) is_<=_than (f . ( sup X)) by A6, A7, A8, YELLOW_0: 30;

      

       A11: (f .: X) is_<=_than (f . ( sup X)) by A9, A10;

       A12:

      now

        let b be Element of T;

        assume

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

        (f .: ( downarrow X)) is_<=_than b

        proof

          let a be Element of T;

          assume a in (f .: ( downarrow X));

          then

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

           A14: x in ( downarrow X) and

           A15: a = (f . x) by FUNCT_1:def 6;

          ( downarrow X) = { z where z be Element of S : ex y be Element of S st z <= y & y in X } by Th14;

          then

          consider z be Element of S such that

           A16: x = z and

           A17: ex y be Element of S st z <= y & y in X by A14;

          consider y be Element of S such that

           A18: z <= y and

           A19: y in X by A17;

          

           A20: f is monotone by A1, Th72;

          

           A21: (f . y) in (f .: X) by A19, FUNCT_2: 35;

          

           A22: (f . z) <= (f . y) by A18, A20;

          (f . y) <= b by A13, A21;

          hence thesis by A15, A16, A22, ORDERS_2: 3;

        end;

        hence (f . ( sup X)) <= b by A6, A7, A8, YELLOW_0: 30;

      end;

      hence ex_sup_of ((f .: X),T) by A11, YELLOW_0: 15;

      hence thesis by A11, A12, YELLOW_0:def 9;

    end;

    theorem :: WAYBEL_0:74

    for S be sup-Semilattice, T be non empty Poset, f be Function of S, T st (for X be finite Subset of S holds f preserves_sup_of X) & (for X be non empty directed Subset of S holds f preserves_sup_of X) holds f is sups-preserving

    proof

      let S be sup-Semilattice, T be non empty Poset, f be Function of S, T such that

       A1: for X be finite Subset of S holds f preserves_sup_of X and

       A2: for X be non empty directed Subset of S holds f preserves_sup_of X;

      let X be Subset of S such that

       A3: ex_sup_of (X,S);

      defpred P[ object] means ex Y be finite Subset of X st ex_sup_of (Y,S) & $1 = ( "\/" (Y,S));

      consider Z be set such that

       A4: for x be object holds x in Z iff x in the carrier of S & P[x] from XBOOLE_0:sch 1;

      Z c= the carrier of S by A4;

      then

      reconsider Z as Subset of S;

       A5:

      now

        let Y be finite Subset of X;

        Y is Subset of S by XBOOLE_1: 1;

        hence Y <> {} implies ex_sup_of (Y,S) by YELLOW_0: 54;

      end;

       A6:

      now

        let Y be finite Subset of X;

        reconsider Y9 = Y as Subset of S by XBOOLE_1: 1;

        assume Y <> {} ;

        then ex_sup_of (Y9,S) by YELLOW_0: 54;

        hence ( "\/" (Y,S)) in Z by A4;

      end;

      

       A7: for x be Element of S st x in Z holds ex Y be finite Subset of X st ex_sup_of (Y,S) & x = ( "\/" (Y,S)) by A4;

      then

       A8: Z is directed by A5, A6, Th51;

      

       A9: ex_sup_of (Z,S) by A3, A5, A6, A7, Th53;

      Z = {} or Z <> {} ;

      then

       A10: f preserves_sup_of Z by A1, A2, A8;

      then

       A11: ex_sup_of ((f .: Z),T) by A9;

      

       A12: ( sup (f .: Z)) = (f . ( sup Z)) by A9, A10;

      

       A13: ( sup Z) = ( sup X) by A3, A5, A6, A7, Th54;

      X c= Z

      proof

        let x be object;

        assume

         A14: x in X;

        then

        reconsider Y = {x} as finite Subset of X by ZFMISC_1: 31;

        reconsider x as Element of S by A14;

        Y is Subset of S by XBOOLE_1: 1;

        then

         A15: ex_sup_of (Y,S) by YELLOW_0: 54;

        x = ( "\/" (Y,S)) by YELLOW_0: 39;

        hence thesis by A4, A15;

      end;

      then

       A16: (f .: X) c= (f .: Z) by RELAT_1: 123;

      

       A17: (f .: Z) is_<=_than (f . ( sup X)) by A11, A12, A13, YELLOW_0: 30;

      

       A18: (f .: X) is_<=_than (f . ( sup X)) by A16, A17;

       A19:

      now

        let b be Element of T;

        assume

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

        (f .: Z) is_<=_than b

        proof

          let a be Element of T;

          assume a in (f .: Z);

          then

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

           A21: x in Z and

           A22: a = (f . x) by FUNCT_1:def 6;

          consider Y be finite Subset of X such that

           A23: ex_sup_of (Y,S) and

           A24: x = ( "\/" (Y,S)) by A4, A21;

          reconsider Y as Subset of S by XBOOLE_1: 1;

          

           A25: (f .: Y) c= (f .: X) by RELAT_1: 123;

          

           A26: f preserves_sup_of Y by A1;

          

           A27: b is_>=_than (f .: Y) by A20, A25;

          

           A28: a = ( "\/" ((f .: Y),T)) by A22, A23, A24, A26;

           ex_sup_of ((f .: Y),T) by A23, A26;

          hence thesis by A27, A28, YELLOW_0:def 9;

        end;

        hence (f . ( sup X)) <= b by A11, A12, A13, YELLOW_0: 30;

      end;

      hence ex_sup_of ((f .: X),T) by A18, YELLOW_0: 15;

      hence thesis by A18, A19, YELLOW_0:def 9;

    end;

    begin

    definition

      let L be non empty reflexive RelStr;

      :: WAYBEL_0:def39

      attr L is up-complete means for X be non empty directed Subset of L holds ex x be Element of L st x is_>=_than X & for y be Element of L st y is_>=_than X holds x <= y;

    end

    registration

      cluster up-complete -> upper-bounded for with_suprema reflexive RelStr;

      coherence

      proof

        let L be with_suprema reflexive RelStr such that

         A1: L is up-complete;

        ( [#] L) = the carrier of L;

        then ex x be Element of L st x is_>=_than the carrier of L & for y be Element of L st y is_>=_than the carrier of L holds x <= y by A1;

        hence ex x be Element of L st x is_>=_than the carrier of L;

      end;

    end

    theorem :: WAYBEL_0:75

    for L be non empty reflexive antisymmetric RelStr holds L is up-complete iff for X be non empty directed Subset of L holds ex_sup_of (X,L)

    proof

      let L be non empty reflexive antisymmetric RelStr;

      hereby

        assume

         A1: L is up-complete;

        let X be non empty directed Subset of L;

        consider x be Element of L such that

         A2: x is_>=_than X and

         A3: for y be Element of L st y is_>=_than X holds x <= y by A1;

        thus ex_sup_of (X,L)

        proof

          take x;

          thus X is_<=_than x & for b be Element of L st X is_<=_than b holds b >= x by A2, A3;

          let c be Element of L;

          assume that

           A4: X is_<=_than c and

           A5: for b be Element of L st X is_<=_than b holds b >= c;

          

           A6: c <= x by A2, A5;

          c >= x by A3, A4;

          hence thesis by A6, ORDERS_2: 2;

        end;

      end;

      assume

       A7: for X be non empty directed Subset of L holds ex_sup_of (X,L);

      let X be non empty directed Subset of L;

       ex_sup_of (X,L) by A7;

      then ex a be Element of L st X is_<=_than a & (for b be Element of L st X is_<=_than b holds b >= a) & for c be Element of L st X is_<=_than c & for b be Element of L st X is_<=_than b holds b >= c holds c = a;

      hence thesis;

    end;

    definition

      let L be non empty reflexive RelStr;

      :: WAYBEL_0:def40

      attr L is /\-complete means for X be non empty Subset of L holds ex x be Element of L st x is_<=_than X & for y be Element of L st y is_<=_than X holds x >= y;

    end

    theorem :: WAYBEL_0:76

    

     Th76: for L be non empty reflexive antisymmetric RelStr holds L is /\-complete iff for X be non empty Subset of L holds ex_inf_of (X,L)

    proof

      let L be non empty reflexive antisymmetric RelStr;

      hereby

        assume

         A1: L is /\-complete;

        let X be non empty Subset of L;

        consider x be Element of L such that

         A2: x is_<=_than X and

         A3: for y be Element of L st y is_<=_than X holds x >= y by A1;

        thus ex_inf_of (X,L)

        proof

          take x;

          thus X is_>=_than x & for b be Element of L st X is_>=_than b holds b <= x by A2, A3;

          let c be Element of L;

          assume that

           A4: X is_>=_than c and

           A5: for b be Element of L st X is_>=_than b holds b <= c;

          

           A6: c <= x by A3, A4;

          c >= x by A2, A5;

          hence thesis by A6, ORDERS_2: 2;

        end;

      end;

      assume

       A7: for X be non empty Subset of L holds ex_inf_of (X,L);

      let X be non empty Subset of L;

       ex_inf_of (X,L) by A7;

      then ex a be Element of L st X is_>=_than a & (for b be Element of L st X is_>=_than b holds b <= a) & for c be Element of L st X is_>=_than c & for b be Element of L st X is_>=_than b holds b <= c holds c = a;

      hence thesis;

    end;

    registration

      cluster complete -> up-complete /\-complete for non empty reflexive RelStr;

      coherence

      proof

        let L be non empty reflexive RelStr such that

         A1: L is complete;

        thus L is up-complete by A1;

        let X be non empty Subset of L;

        set Y = { y where y be Element of L : y is_<=_than X };

        consider x be Element of L such that

         A2: Y is_<=_than x and

         A3: for b be Element of L st Y is_<=_than b holds x <= b by A1;

        take x;

        thus x is_<=_than X

        proof

          let y be Element of L such that

           A4: y in X;

          y is_>=_than Y

          proof

            let z be Element of L;

            assume z in Y;

            then ex a be Element of L st z = a & a is_<=_than X;

            hence thesis by A4;

          end;

          hence x <= y by A3;

        end;

        let y be Element of L;

        assume y is_<=_than X;

        then y in Y;

        hence thesis by A2;

      end;

      cluster /\-complete -> lower-bounded for non empty reflexive RelStr;

      coherence

      proof

        let L be non empty reflexive RelStr;

        assume L is /\-complete;

        then ex x be Element of L st x is_<=_than ( [#] L) & for y be Element of L st y is_<=_than ( [#] L) holds x >= y;

        hence ex x be Element of L st x is_<=_than the carrier of L;

      end;

      cluster up-complete with_suprema lower-bounded -> complete for non empty Poset;

      coherence

      proof

        let L be non empty Poset;

        assume

         A5: L is up-complete with_suprema lower-bounded;

        then

        reconsider K = L as with_suprema lower-bounded non empty Poset;

        let X be set;

        reconsider X9 = (X /\ the carrier of L) as Subset of L by XBOOLE_1: 17;

        reconsider A = X9 as Subset of K;

         A6:

        now

          let Y be finite Subset of X9;

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

          hence Y <> {} implies ex_sup_of (Y,L) by A5, YELLOW_0: 54;

        end;

         A7:

        now

          let x be Element of L;

          assume x in ( finsups X9);

          then ex Y be finite Subset of X9 st x = ( "\/" (Y,L)) & ex_sup_of (Y,L);

          hence ex Y be finite Subset of X9 st ex_sup_of (Y,L) & x = ( "\/" (Y,L));

        end;

         A8:

        now

          let Y be finite Subset of X9;

          reconsider Z = Y as Subset of L by XBOOLE_1: 1;

          assume Y <> {} ;

          then ex_sup_of (Z,L) by A5, YELLOW_0: 54;

          hence ( "\/" (Y,L)) in ( finsups X9);

        end;

        reconsider fX = ( finsups A) as non empty directed Subset of L;

        consider x be Element of L such that

         A9: fX is_<=_than x and

         A10: for y be Element of L st fX is_<=_than y holds x <= y by A5;

        take x;

        X9 is_<=_than x by A6, A7, A8, A9, Th52;

        hence X is_<=_than x by YELLOW_0: 5;

        let y be Element of L;

        assume y is_>=_than X;

        then y is_>=_than X9 by YELLOW_0: 5;

        then y is_>=_than fX by A6, A7, A8, Th52;

        hence thesis by A10;

      end;

    end

    registration

      cluster /\-complete -> with_infima for non empty reflexive antisymmetric RelStr;

      coherence

      proof

        let L be non empty reflexive antisymmetric RelStr;

        assume L is /\-complete;

        then for a,b be Element of L holds ex_inf_of ( {a, b},L) by Th76;

        hence thesis by YELLOW_0: 21;

      end;

    end

    registration

      cluster /\-complete -> with_suprema for non empty reflexive antisymmetric upper-bounded RelStr;

      coherence

      proof

        let L be non empty reflexive antisymmetric upper-bounded RelStr such that

         A1: L is /\-complete;

        now

          let a,b be Element of L;

          set X = { x where x be Element of L : x >= a & x >= b };

          X c= the carrier of L

          proof

            let x be object;

            assume x in X;

            then ex z be Element of L st x = z & z >= a & z >= b;

            hence thesis;

          end;

          then

          reconsider X as Subset of L;

          

           A2: ( Top L) >= a by YELLOW_0: 45;

          ( Top L) >= b by YELLOW_0: 45;

          then ( Top L) in X by A2;

          then ex_inf_of (X,L) by A1, Th76;

          then

          consider c be Element of L such that

           A3: c is_<=_than X and

           A4: for d be Element of L st d is_<=_than X holds d <= c and for e be Element of L st e is_<=_than X & for d be Element of L st d is_<=_than X holds d <= e holds e = c;

          

           A5: c is_>=_than {a, b}

          proof

            let x be Element of L;

            assume

             A6: x in {a, b};

            x is_<=_than X

            proof

              let y be Element of L;

              assume y in X;

              then ex z be Element of L st y = z & z >= a & z >= b;

              hence thesis by A6, TARSKI:def 2;

            end;

            hence thesis by A4;

          end;

          now

            let y be Element of L;

            assume

             A7: y is_>=_than {a, b};

            then

             A8: y >= a by YELLOW_0: 8;

            y >= b by A7, YELLOW_0: 8;

            then y in X by A8;

            hence c <= y by A3;

          end;

          hence ex_sup_of ( {a, b},L) by A5, YELLOW_0: 15;

        end;

        hence thesis by YELLOW_0: 20;

      end;

    end

    registration

      cluster complete strict for LATTICE;

      existence

      proof

        set L = the complete strict LATTICE;

        take L;

        thus thesis;

      end;

    end