yellow_0.miz

    begin

    scheme :: YELLOW_0:sch1

    RelStrEx { X() -> non empty set , P[ set, set] } :

ex L be non empty strict RelStr st the carrier of L = X() & for a,b be Element of L holds a <= b iff P[a, b];

      consider R be Relation of X() such that

       A1: for a,b be Element of X() holds [a, b] in R iff P[a, b] from RELSET_1:sch 2;

      take L = RelStr (# X(), R #);

      thus the carrier of L = X();

      let a,b be Element of L;

      thus thesis by A1;

    end;

    definition

      let A be non empty RelStr;

      :: original: reflexive

      redefine

      :: YELLOW_0:def1

      attr A is reflexive means for x be Element of A holds x <= x;

      compatibility

      proof

        thus A is reflexive implies for x be Element of A holds x <= x by ORDERS_2: 1;

        assume

         A1: for x be Element of A holds x <= x;

        let x be object;

        assume x in the carrier of A;

        then

        reconsider x as Element of A;

        x <= x by A1;

        hence thesis;

      end;

    end

    definition

      let A be RelStr;

      :: original: transitive

      redefine

      :: YELLOW_0:def2

      attr A is transitive means for x,y,z be Element of A st x <= y & y <= z holds x <= z;

      compatibility

      proof

        thus A is transitive implies for x,y,z be Element of A st x <= y & y <= z holds x <= z by ORDERS_2: 3;

        assume

         A1: for x,y,z be Element of A st x <= y & y <= z holds x <= z;

        let x,y,z be object;

        assume

         A2: x in the carrier of A & y in the carrier of A & z in the carrier of A;

        assume

         A3: [x, y] in the InternalRel of A & [y, z] in the InternalRel of A;

        reconsider x, y, z as Element of A by A2;

        x <= y & y <= z by A3;

        then x <= z by A1;

        hence thesis;

      end;

      :: original: antisymmetric

      redefine

      :: YELLOW_0:def3

      attr A is antisymmetric means for x,y be Element of A st x <= y & y <= x holds x = y;

      compatibility

      proof

        thus A is antisymmetric implies for x,y be Element of A st x <= y & y <= x holds x = y by ORDERS_2: 2;

        assume

         A4: for x,y be Element of A st x <= y & y <= x holds x = y;

        let x,y be object;

        assume

         A5: x in the carrier of A & y in the carrier of A;

        assume

         A6: [x, y] in the InternalRel of A & [y, x] in the InternalRel of A;

        reconsider x, y as Element of A by A5;

        x <= y & y <= x by A6;

        hence thesis by A4;

      end;

    end

    registration

      cluster complete -> with_suprema with_infima for non empty RelStr;

      coherence by LATTICE3: 12;

      cluster -> complete transitive antisymmetric for 1 -element reflexive RelStr;

      coherence

      proof

        let L be 1 -element reflexive RelStr;

        set x = the Element of L;



         A1: for x,y be Element of L holds x = y by STRUCT_0:def 10;

        thus L is complete

        proof

          let X be set;

          take x;

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

          let y be Element of L;

          y = x by A1;

          hence thesis by ORDERS_2: 1;

        end;

        thus L is transitive by A1;

        let x be Element of L;

        thus thesis by A1;

      end;

    end

    registration

      let x be set;

      let R be Relation of {x};

      cluster RelStr (# {x}, R #) -> 1 -element;

      coherence ;

    end

    registration

      cluster strict1 -element reflexive for RelStr;

      existence

      proof

        set O = the Order of { {} };

        take RelStr (# { {} }, O #);

        thus thesis;

      end;

    end

    theorem :: YELLOW_0:1



     Th1: for P1,P2 be RelStr st the RelStr of P1 = the RelStr of P2 holds for a1,b1 be Element of P1 holds for a2,b2 be Element of P2 st a1 = a2 & b1 = b2 holds (a1 <= b1 implies a2 <= b2) & (a1 < b1 implies a2 < b2)

    proof

      let P1,P2 be RelStr such that

       A1: the RelStr of P1 = the RelStr of P2;

      let a1,b1 be Element of P1;

      let a2,b2 be Element of P2;



       A2: a2 <= b2 iff [a2, b2] in the InternalRel of P2;

      a1 <= b1 iff [a1, b1] in the InternalRel of P1;

      hence thesis by A1, A2;

    end;

    theorem :: YELLOW_0:2



     Th2: for P1,P2 be RelStr st the RelStr of P1 = the RelStr of P2 holds for X be set holds for a1 be Element of P1 holds for a2 be Element of P2 st a1 = a2 holds (X is_<=_than a1 implies X is_<=_than a2) & (X is_>=_than a1 implies X is_>=_than a2) by Th1;

    theorem :: YELLOW_0:3

    for P1,P2 be RelStr st the RelStr of P1 = the RelStr of P2 & P1 is complete holds P2 is complete

    proof

      let P1,P2 be RelStr such that

       A1: the RelStr of P1 = the RelStr of P2 and

       A2: for X be set holds ex a be Element of P1 st X is_<=_than a & for b be Element of P1 st X is_<=_than b holds a <= b;

      let X be set;

      consider a be Element of P1 such that

       A3: X is_<=_than a and

       A4: for b be Element of P1 st X is_<=_than b holds a <= b by A2;

      reconsider a9 = a as Element of P2 by A1;

      take a9;

      thus X is_<=_than a9 by A1, A3, Th2;

      let b9 be Element of P2;

      reconsider b = b9 as Element of P1 by A1;

      assume X is_<=_than b9;

      then a <= b by A1, A4, Th2;

      hence thesis by A1;

    end;

    theorem :: YELLOW_0:4



     Th4: for L be transitive RelStr, x,y be Element of L st x <= y holds for X be set holds (y is_<=_than X implies x is_<=_than X) & (x is_>=_than X implies y is_>=_than X)

    proof

      let L be transitive RelStr, x,y be Element of L;

      assume

       A1: x <= y;

      let X be set;

      hereby

        assume

         A2: y is_<=_than X;

        thus x is_<=_than X

        proof

          let z be Element of L;

          assume z in X;

          then z >= y by A2;

          hence thesis by A1, ORDERS_2: 3;

        end;

      end;

      assume

       A3: x is_>=_than X;

      let z be Element of L;

      assume z in X;

      then x >= z by A3;

      hence thesis by A1, ORDERS_2: 3;

    end;

    theorem :: YELLOW_0:5



     Th5: for L be non empty RelStr, X be set, x be Element of L holds (x is_>=_than X iff x is_>=_than (X /\ the carrier of L)) & (x is_<=_than X iff x is_<=_than (X /\ the carrier of L))

    proof

      let L be non empty RelStr, X be set, x be Element of L;

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

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

      proof

        assume

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

        let b be Element of L;

        assume b in Y;

        then b in X by XBOOLE_0:def 4;

        hence thesis by A1;

      end;

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

      proof

        assume

         A2: for b be Element of L st b in Y holds b <= x;

        let b be Element of L;

        assume b in X;

        then b in Y by XBOOLE_0:def 4;

        hence thesis by A2;

      end;

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

      proof

        assume

         A3: for b be Element of L st b in X holds b >= x;

        let b be Element of L;

        assume b in Y;

        then b in X by XBOOLE_0:def 4;

        hence thesis by A3;

      end;

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

      proof

        assume

         A4: for b be Element of L st b in Y holds b >= x;

        let b be Element of L;

        assume b in X;

        then b in Y by XBOOLE_0:def 4;

        hence thesis by A4;

      end;

    end;

    theorem :: YELLOW_0:6



     Th6: for L be RelStr, a be Element of L holds {} is_<=_than a & {} is_>=_than a;

    theorem :: YELLOW_0:7



     Th7: for L be RelStr, a,b be Element of L holds (a is_<=_than {b} iff a <= b) & (a is_>=_than {b} iff b <= a)

    proof

      let L be RelStr, a,b be Element of L;



       A1: b in {b} by TARSKI:def 1;

      hence a is_<=_than {b} implies a <= b;

      thus a <= b implies a is_<=_than {b} by TARSKI:def 1;

      thus a is_>=_than {b} implies a >= b by A1;

      assume

       A2: a >= b;

      let c be Element of L;

      thus thesis by A2, TARSKI:def 1;

    end;

    theorem :: YELLOW_0:8



     Th8: for L be RelStr, a,b,c be Element of L holds (a is_<=_than {b, c} iff a <= b & a <= c) & (a is_>=_than {b, c} iff b <= a & c <= a)

    proof

      let L be RelStr, a,b,c be Element of L;



       A1: b in {b, c} & c in {b, c} by TARSKI:def 2;

      hence a is_<=_than {b, c} implies a <= b & a <= c;

      thus a <= b & a <= c implies a is_<=_than {b, c} by TARSKI:def 2;

      thus a is_>=_than {b, c} implies a >= b & a >= c by A1;

      assume

       A2: a >= b & a >= c;

      let c be Element of L;

      thus thesis by A2, TARSKI:def 2;

    end;

    theorem :: YELLOW_0:9

    for L be RelStr, X,Y be set st X c= Y holds for x be Element of L holds (x is_<=_than Y implies x is_<=_than X) & (x is_>=_than Y implies x is_>=_than X);

    theorem :: YELLOW_0:10



     Th10: for L be RelStr, X,Y be set, x be Element of L holds (x is_<=_than X & x is_<=_than Y implies x is_<=_than (X \/ Y)) & (x is_>=_than X & x is_>=_than Y implies x is_>=_than (X \/ Y))

    proof

      let L be RelStr, X,Y be set, x be Element of L;

      thus x is_<=_than X & x is_<=_than Y implies x is_<=_than (X \/ Y)

      proof

        assume

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

        let y be Element of L;

        y in (X \/ Y) implies y in X or y in Y by XBOOLE_0:def 3;

        hence thesis by A1;

      end;

      assume

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

      let y be Element of L;

      y in (X \/ Y) implies y in X or y in Y by XBOOLE_0:def 3;

      hence thesis by A2;

    end;

    theorem :: YELLOW_0:11



     Th11: for L be transitive RelStr holds for X be set, x,y be Element of L st X is_<=_than x & x <= y holds X is_<=_than y

    proof

      let L be transitive RelStr;

      let X be set, x,y be Element of L such that

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

       A2: x <= y;

      let z be Element of L;

      assume z in X;

      then z <= x by A1;

      hence thesis by A2, ORDERS_2: 3;

    end;

    theorem :: YELLOW_0:12



     Th12: for L be transitive RelStr holds for X be set, x,y be Element of L st X is_>=_than x & x >= y holds X is_>=_than y

    proof

      let L be transitive RelStr;

      let X be set, x,y be Element of L such that

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

       A2: x >= y;

      let z be Element of L;

      assume z in X;

      then z >= x by A1;

      hence thesis by A2, ORDERS_2: 3;

    end;

    registration

      let L be non empty RelStr;

      cluster ( [#] L) -> non empty;

      coherence ;

    end

    begin

    definition

      let L be RelStr;

      :: YELLOW_0:def4

      attr L is lower-bounded means

      : Def4: ex x be Element of L st x is_<=_than the carrier of L;

      :: YELLOW_0:def5

      attr L is upper-bounded means

      : Def5: ex x be Element of L st x is_>=_than the carrier of L;

    end

    definition

      let L be RelStr;

      :: YELLOW_0:def6

      attr L is bounded means L is lower-bounded upper-bounded;

    end

    theorem :: YELLOW_0:13

    for P1,P2 be RelStr st the RelStr of P1 = the RelStr of P2 holds (P1 is lower-bounded implies P2 is lower-bounded) & (P1 is upper-bounded implies P2 is upper-bounded) by Th2;

    registration

      cluster complete -> bounded for non empty RelStr;

      coherence

      proof

        let L be non empty RelStr;

        assume

         A1: for X be set holds ex a be Element of L st X is_<=_than a & for b be Element of L st X is_<=_than b holds a <= b;

        then

        consider a0 be Element of L such that {} is_<=_than a0 and

         A2: for b be Element of L st {} is_<=_than b holds a0 <= b;

        consider a1 be Element of L such that

         A3: the carrier of L is_<=_than a1 and for b be Element of L st the carrier of L is_<=_than b holds a1 <= b by A1;

        reconsider a0, a1 as Element of L;

        hereby

          take a0;

          thus a0 is_<=_than the carrier of L by A2, Th6;

        end;

        take a1;

        thus thesis by A3;

      end;

      cluster bounded -> lower-bounded upper-bounded for RelStr;

      coherence ;

      cluster lower-bounded upper-bounded -> bounded for RelStr;

      coherence ;

    end

    registration

      cluster complete for non empty Poset;

      existence

      proof

        set L = the complete non empty Poset;

        take L;

        thus thesis;

      end;

    end

    definition

      let L be RelStr;

      let X be set;

      :: YELLOW_0:def7

      pred ex_sup_of X,L means 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;

      :: YELLOW_0:def8

      pred ex_inf_of X,L means 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;

    end

    theorem :: YELLOW_0:14



     Th14: for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 holds for X be set holds ( ex_sup_of (X,L1) implies ex_sup_of (X,L2)) & ( ex_inf_of (X,L1) implies ex_inf_of (X,L2))

    proof

      let L1,L2 be RelStr such that

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

      let X be set;

      thus ex_sup_of (X,L1) implies ex_sup_of (X,L2)

      proof

        given a be Element of L1 such that

         A2: X is_<=_than a and

         A3: for b be Element of L1 st X is_<=_than b holds b >= a and

         A4: for c be Element of L1 st X is_<=_than c & for b be Element of L1 st X is_<=_than b holds b >= c holds c = a;

        reconsider a9 = a as Element of L2 by A1;

        take a9;

        thus X is_<=_than a9 by A1, A2, Th2;

        hereby

          let b9 be Element of L2;

          reconsider b = b9 as Element of L1 by A1;

          assume X is_<=_than b9;

          then b >= a by A1, A3, Th2;

          hence b9 >= a9 by A1;

        end;

        let c9 be Element of L2;

        reconsider c = c9 as Element of L1 by A1;

        assume X is_<=_than c9;

        then

         A5: X is_<=_than c by A1, Th2;

        assume

         A6: for b9 be Element of L2 st X is_<=_than b9 holds b9 >= c9;

        now

          let b be Element of L1;

          reconsider b9 = b as Element of L2 by A1;

          assume X is_<=_than b;

          then b9 >= c9 by A1, A6, Th2;

          hence b >= c by A1;

        end;

        hence thesis by A4, A5;

      end;

      given a be Element of L1 such that

       A7: X is_>=_than a and

       A8: for b be Element of L1 st X is_>=_than b holds b <= a and

       A9: for c be Element of L1 st X is_>=_than c & for b be Element of L1 st X is_>=_than b holds b <= c holds c = a;

      reconsider a9 = a as Element of L2 by A1;

      take a9;

      thus X is_>=_than a9 by A1, A7, Th2;

      hereby

        let b9 be Element of L2;

        reconsider b = b9 as Element of L1 by A1;

        assume X is_>=_than b9;

        then b <= a by A1, A8, Th2;

        hence b9 <= a9 by A1;

      end;

      let c9 be Element of L2;

      reconsider c = c9 as Element of L1 by A1;

      assume

       A10: X is_>=_than c9;

      assume

       A11: for b9 be Element of L2 st X is_>=_than b9 holds b9 <= c9;

       A12:

      now

        let b be Element of L1;

        reconsider b9 = b as Element of L2 by A1;

        assume X is_>=_than b;

        then b9 <= c9 by A1, A11, Th2;

        hence b <= c by A1;

      end;

      X is_>=_than c by A1, A10, Th2;

      hence thesis by A9, A12;

    end;

    theorem :: YELLOW_0:15



     Th15: for L be antisymmetric RelStr, X be set holds ex_sup_of (X,L) iff ex a be Element of L st X is_<=_than a & for b be Element of L st X is_<=_than b holds a <= b

    proof

      let L be antisymmetric RelStr, X be set;

      thus ex_sup_of (X,L) implies ex a be Element of L st X is_<=_than a & for b be Element of L st X is_<=_than b holds a <= b;

      given a be Element of L such that

       A1: X is_<=_than a & for b be Element of L st X is_<=_than b holds a <= b;

      take a;

      thus X is_<=_than a & for b be Element of L st X is_<=_than b holds b >= a by A1;

      let c be Element of L;

      assume X is_<=_than c & for b be Element of L st X is_<=_than b holds b >= c;

      then a <= c & c <= a by A1;

      hence thesis by ORDERS_2: 2;

    end;

    theorem :: YELLOW_0:16



     Th16: for L be antisymmetric RelStr, X be set holds ex_inf_of (X,L) iff ex a be Element of L st X is_>=_than a & for b be Element of L st X is_>=_than b holds a >= b

    proof

      let L be antisymmetric RelStr, X be set;

      thus ex_inf_of (X,L) implies ex a be Element of L st X is_>=_than a & for b be Element of L st X is_>=_than b holds a >= b;

      given a be Element of L such that

       A1: X is_>=_than a & for b be Element of L st X is_>=_than b holds a >= b;

      take a;

      thus X is_>=_than a & for b be Element of L st X is_>=_than b holds a >= b by A1;

      let c be Element of L;

      assume X is_>=_than c & for b be Element of L st X is_>=_than b holds c >= b;

      then a <= c & c <= a by A1;

      hence thesis by ORDERS_2: 2;

    end;

    theorem :: YELLOW_0:17



     Th17: for L be complete non empty antisymmetric RelStr, X be set holds ex_sup_of (X,L) & ex_inf_of (X,L)

    proof

      let L be complete non empty antisymmetric RelStr, X be set;

      set Y = { c where c be Element of L : c is_<=_than X };

      consider a be Element of L such that

       A1: Y is_<=_than a and

       A2: for b be Element of L st Y is_<=_than b holds a <= b by LATTICE3:def 12;

      ex a be Element of L st X is_<=_than a & for b be Element of L st X is_<=_than b holds a <= b by LATTICE3:def 12;

      hence ex_sup_of (X,L) by Th15;

      now

        take a;

        thus a is_<=_than X

        proof

          let b be Element of L;

          assume

           A3: b in X;

          Y is_<=_than b

          proof

            let c be Element of L;

            assume c in Y;

            then ex d be Element of L st c = d & d is_<=_than X;

            hence thesis by A3;

          end;

          hence thesis by A2;

        end;

        let b be Element of L;

        assume b is_<=_than X;

        then b in Y;

        hence b <= a by A1;

      end;

      hence thesis by Th16;

    end;

    theorem :: YELLOW_0:18



     Th18: for L be antisymmetric RelStr holds for a,b,c be Element of L holds c = (a "\/" b) & ex_sup_of ( {a, b},L) iff c >= a & c >= b & for d be Element of L st d >= a & d >= b holds c <= d

    proof

      let L be antisymmetric RelStr;

      let a,b,c be Element of L;

      hereby

        assume that

         A1: c = (a "\/" b) and

         A2: ex_sup_of ( {a, b},L);

        consider c1 be Element of L such that

         A3: {a, b} is_<=_than c1 and

         A4: for d be Element of L st {a, b} is_<=_than d holds c1 <= d by A2;

         A5:

        now

          let d be Element of L;

          assume a <= d & b <= d;

          then {a, b} is_<=_than d by Th8;

          hence c1 <= d by A4;

        end;

        a <= c1 & b <= c1 by A3, Th8;

        hence c >= a & c >= b & for d be Element of L st d >= a & d >= b holds c <= d by A1, A5, LATTICE3:def 13;

      end;

      assume that

       A6: c >= a & c >= b and

       A7: for d be Element of L st d >= a & d >= b holds c <= d;

      thus c = (a "\/" b) by A6, A7, LATTICE3:def 13;

      now

        take c;

        thus c is_>=_than {a, b} by A6, Th8;

        let d be Element of L;

        assume d is_>=_than {a, b};

        then d >= a & d >= b by Th8;

        hence c <= d by A7;

      end;

      hence thesis by Th15;

    end;

    theorem :: YELLOW_0:19



     Th19: for L be antisymmetric RelStr holds for a,b,c be Element of L holds c = (a "/\" b) & ex_inf_of ( {a, b},L) iff c <= a & c <= b & for d be Element of L st d <= a & d <= b holds c >= d

    proof

      let L be antisymmetric RelStr;

      let a,b,c be Element of L;

      hereby

        assume that

         A1: c = (a "/\" b) and

         A2: ex_inf_of ( {a, b},L);

        consider c1 be Element of L such that

         A3: {a, b} is_>=_than c1 and

         A4: for d be Element of L st {a, b} is_>=_than d holds c1 >= d by A2;

         A5:

        now

          let d be Element of L;

          assume a >= d & b >= d;

          then {a, b} is_>=_than d by Th8;

          hence c1 >= d by A4;

        end;

        a >= c1 & b >= c1 by A3, Th8;

        hence c <= a & c <= b & for d be Element of L st d <= a & d <= b holds c >= d by A1, A5, LATTICE3:def 14;

      end;

      assume that

       A6: c <= a & c <= b and

       A7: for d be Element of L st d <= a & d <= b holds c >= d;

      thus c = (a "/\" b) by A6, A7, LATTICE3:def 14;

      now

        take c;

        thus c is_<=_than {a, b} by A6, Th8;

        let d be Element of L;

        assume d is_<=_than {a, b};

        then d <= a & d <= b by Th8;

        hence c >= d by A7;

      end;

      hence thesis by Th16;

    end;

    theorem :: YELLOW_0:20



     Th20: for L be antisymmetric RelStr holds L is with_suprema iff for a,b be Element of L holds ex_sup_of ( {a, b},L)

    proof

      let L be antisymmetric RelStr;

      hereby

        assume

         A1: L is with_suprema;

        let a,b be Element of L;

        ex z be Element of L st a <= z & b <= z & for z9 be Element of L st a <= z9 & b <= z9 holds z <= z9 by A1;

        hence ex_sup_of ( {a, b},L) by Th18;

      end;

      assume

       A2: for a,b be Element of L holds ex_sup_of ( {a, b},L);

      let x,y be Element of L;

      take (x "\/" y);

       ex_sup_of ( {x, y},L) by A2;

      hence thesis by Th18;

    end;

    theorem :: YELLOW_0:21



     Th21: for L be antisymmetric RelStr holds L is with_infima iff for a,b be Element of L holds ex_inf_of ( {a, b},L)

    proof

      let L be antisymmetric RelStr;

      hereby

        assume

         A1: L is with_infima;

        let a,b be Element of L;

        ex z be Element of L st a >= z & b >= z & for z9 be Element of L st a >= z9 & b >= z9 holds z >= z9 by A1;

        hence ex_inf_of ( {a, b},L) by Th19;

      end;

      assume

       A2: for a,b be Element of L holds ex_inf_of ( {a, b},L);

      let x,y be Element of L;

      take (x "/\" y);

       ex_inf_of ( {x, y},L) by A2;

      hence thesis by Th19;

    end;

    theorem :: YELLOW_0:22



     Th22: for L be antisymmetric with_suprema RelStr holds for a,b,c be Element of L holds c = (a "\/" b) iff c >= a & c >= b & for d be Element of L st d >= a & d >= b holds c <= d

    proof

      let A be antisymmetric with_suprema RelStr;

      let a,b be Element of A;

      ex x be Element of A st a <= x & b <= x & for c be Element of A st a <= c & b <= c holds x <= c by LATTICE3:def 10;

      hence thesis by LATTICE3:def 13;

    end;

    theorem :: YELLOW_0:23



     Th23: for L be antisymmetric with_infima RelStr holds for a,b,c be Element of L holds c = (a "/\" b) iff c <= a & c <= b & for d be Element of L st d <= a & d <= b holds c >= d

    proof

      let A be antisymmetric with_infima RelStr;

      let a,b be Element of A;

      ex x be Element of A st a >= x & b >= x & for c be Element of A st a >= c & b >= c holds x >= c by LATTICE3:def 11;

      hence thesis by LATTICE3:def 14;

    end;

    theorem :: YELLOW_0:24

    for L be antisymmetric reflexive with_suprema RelStr holds for a,b be Element of L holds a = (a "\/" b) iff a >= b

    proof

      let L be antisymmetric reflexive with_suprema RelStr;

      let a,b be Element of L;

      a <= a & for d be Element of L st d >= a & d >= b holds a <= d;

      hence thesis by Th22;

    end;

    theorem :: YELLOW_0:25

    for L be antisymmetric reflexive with_infima RelStr holds for a,b be Element of L holds a = (a "/\" b) iff a <= b

    proof

      let L be antisymmetric reflexive with_infima RelStr;

      let a,b be Element of L;

      a <= a & for d be Element of L st d <= a & d <= b holds a >= d;

      hence thesis by Th23;

    end;

    definition

      let L be RelStr;

      let X be set;

      :: YELLOW_0:def9

      func "\/" (X,L) -> Element of L means

      : Def9: X is_<=_than it & for a be Element of L st X is_<=_than a holds it <= a if ex_sup_of (X,L);

      uniqueness

      proof

        let a1,a2 be Element of L;

        given a be Element of L such that X is_<=_than a and for b be Element of L st X is_<=_than b holds b >= a and

         A1: 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;

        assume

         A2: not thesis;

        then a1 = a by A1;

        hence contradiction by A1, A2;

      end;

      existence ;

      correctness ;

      :: YELLOW_0:def10

      func "/\" (X,L) -> Element of L means

      : Def10: X is_>=_than it & for a be Element of L st X is_>=_than a holds a <= it if ex_inf_of (X,L);

      uniqueness

      proof

        let a1,a2 be Element of L;

        given a be Element of L such that X is_>=_than a and for b be Element of L st X is_>=_than b holds b <= a and

         A3: 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;

        assume

         A4: not thesis;

        then a1 = a by A3;

        hence contradiction by A3, A4;

      end;

      existence ;

      correctness ;

    end

    theorem :: YELLOW_0:26

    for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 holds for X be set st ex_sup_of (X,L1) holds ( "\/" (X,L1)) = ( "\/" (X,L2))

    proof

      let L1,L2 be RelStr such that

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

      let X be set;

      reconsider c = ( "\/" (X,L1)) as Element of L2 by A1;

      assume

       A2: ex_sup_of (X,L1);

      then X is_<=_than ( "\/" (X,L1)) by Def9;

      then

       A3: X is_<=_than c by A1, Th2;

       A4:

      now

        let a be Element of L2;

        reconsider b = a as Element of L1 by A1;

        assume X is_<=_than a;

        then X is_<=_than b by A1, Th2;

        then b >= ( "\/" (X,L1)) by A2, Def9;

        hence a >= c by A1;

      end;

       ex_sup_of (X,L2) by A1, A2, Th14;

      hence thesis by A3, A4, Def9;

    end;

    theorem :: YELLOW_0:27

    for L1,L2 be RelStr st the RelStr of L1 = the RelStr of L2 holds for X be set st ex_inf_of (X,L1) holds ( "/\" (X,L1)) = ( "/\" (X,L2))

    proof

      let L1,L2 be RelStr such that

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

      let X be set;

      reconsider c = ( "/\" (X,L1)) as Element of L2 by A1;

      assume

       A2: ex_inf_of (X,L1);

      then X is_>=_than ( "/\" (X,L1)) by Def10;

      then

       A3: X is_>=_than c by A1, Th2;

       A4:

      now

        let a be Element of L2;

        reconsider b = a as Element of L1 by A1;

        assume X is_>=_than a;

        then X is_>=_than b by A1, Th2;

        then b <= ( "/\" (X,L1)) by A2, Def10;

        hence a <= c by A1;

      end;

       ex_inf_of (X,L2) by A1, A2, Th14;

      hence thesis by A3, A4, Def10;

    end;

    theorem :: YELLOW_0:28

    for L be complete non empty Poset, X be set holds ( "\/" (X,L)) = ( "\/" (X,( latt L))) & ( "/\" (X,L)) = ( "/\" (X,( latt L)))

    proof

      let L be complete non empty Poset, X be set;



       A1: the RelStr of L = ( LattPOSet ( latt L)) by LATTICE3:def 15;

      then

      reconsider x = ( "\/" (X,L)) as Element of ( LattPOSet ( latt L));

      reconsider y = ( "/\" (X,( latt L))) as Element of L by A1;

       A2:

      now

        let a be Element of L;

        reconsider a9 = a as Element of ( LattPOSet ( latt L)) by A1;

        assume a is_<=_than X;

        then a9 is_<=_than X by A1, Th2;

        then ( % a9) is_less_than X by LATTICE3: 29;

        then

         A3: ( % a9) [= ( "/\" (X,( latt L))) by LATTICE3: 34;

        (( % a9) % ) = ( % a9);

        then a9 <= (( "/\" (X,( latt L))) % ) by A3, LATTICE3: 7;

        hence a <= y by A1;

      end;

      ex a be Element of L st X is_<=_than a & for b be Element of L st X is_<=_than b holds a <= b by LATTICE3:def 12;

      then

       A4: ex_sup_of (X,L) by Th15;

       A5:

      now

        let a be Element of ( latt L);

        reconsider a9 = (a % ) as Element of L by A1;

        assume X is_less_than a;

        then X is_<=_than (a % ) by LATTICE3: 30;

        then X is_<=_than a9 by A1, Th2;

        then ( "\/" (X,L)) <= a9 by A4, Def9;

        then

         A6: x <= (a % ) by A1;

        (( % x) % ) = ( % x);

        hence ( % x) [= a by A6, LATTICE3: 7;

      end;

      X is_<=_than ( "\/" (X,L)) by A4, Def9;

      then X is_<=_than x by A1, Th2;

      then X is_less_than ( % x) by LATTICE3: 31;

      hence ( "\/" (X,L)) = ( "\/" (X,( latt L))) by A5, LATTICE3:def 21;

      ( "/\" (X,( latt L))) is_less_than X by LATTICE3: 34;

      then (( "/\" (X,( latt L))) % ) is_<=_than X by LATTICE3: 28;

      then

       A7: y is_<=_than X by A1, Th2;

      then ex_inf_of (X,L) by A2, Th16;

      hence thesis by A7, A2, Def10;

    end;

    theorem :: YELLOW_0:29

    for L be complete Lattice, X be set holds ( "\/" (X,L)) = ( "\/" (X,( LattPOSet L))) & ( "/\" (X,L)) = ( "/\" (X,( LattPOSet L)))

    proof

      let L be complete Lattice, X be set;

       A1:

      now

        let r be Element of ( LattPOSet L);

        assume X is_<=_than r;

        then X is_less_than ( % r) by LATTICE3: 31;

        then

         A2: ( "\/" (X,L)) [= ( % r) by LATTICE3:def 21;

        (( % r) % ) = ( % r);

        hence (( "\/" (X,L)) % ) <= r by A2, LATTICE3: 7;

      end;

      X is_less_than ( "\/" (X,L)) by LATTICE3:def 21;

      then

       A3: X is_<=_than (( "\/" (X,L)) % ) by LATTICE3: 30;

      then ex_sup_of (X,( LattPOSet L)) by A1, Th15;

      hence ( "\/" (X,L)) = ( "\/" (X,( LattPOSet L))) by A3, A1, Def9;

       A4:

      now

        let r be Element of ( LattPOSet L);

        assume X is_>=_than r;

        then X is_greater_than ( % r) by LATTICE3: 29;

        then

         A5: ( % r) [= ( "/\" (X,L)) by LATTICE3: 34;

        (( % r) % ) = ( % r);

        hence (( "/\" (X,L)) % ) >= r by A5, LATTICE3: 7;

      end;

      X is_greater_than ( "/\" (X,L)) by LATTICE3: 34;

      then

       A6: X is_>=_than (( "/\" (X,L)) % ) by LATTICE3: 28;

      then ex_inf_of (X,( LattPOSet L)) by A4, Th16;

      hence thesis by A6, A4, Def10;

    end;

    theorem :: YELLOW_0:30



     Th30: for L be antisymmetric RelStr holds for a be Element of L, X be set holds a = ( "\/" (X,L)) & ex_sup_of (X,L) iff a is_>=_than X & for b be Element of L st b is_>=_than X holds a <= b

    proof

      let L be antisymmetric RelStr;

      let a be Element of L, X be set;

      (a is_>=_than X & for b be Element of L st b is_>=_than X holds a <= b) implies ex_sup_of (X,L) by Th15;

      hence thesis by Def9;

    end;

    theorem :: YELLOW_0:31



     Th31: for L be antisymmetric RelStr holds for a be Element of L, X be set holds a = ( "/\" (X,L)) & ex_inf_of (X,L) iff a is_<=_than X & for b be Element of L st b is_<=_than X holds a >= b

    proof

      let L be antisymmetric RelStr;

      let a be Element of L, X be set;

      (a is_<=_than X & for b be Element of L st b is_<=_than X holds a >= b) implies ex_inf_of (X,L) by Th16;

      hence thesis by Def10;

    end;

    theorem :: YELLOW_0:32

    for L be complete antisymmetric non empty RelStr holds for a be Element of L, X be set holds a = ( "\/" (X,L)) iff a is_>=_than X & for b be Element of L st b is_>=_than X holds a <= b

    proof

      let L be complete antisymmetric non empty RelStr;

      let a be Element of L, X be set;

       ex_sup_of (X,L) by Th17;

      hence thesis by Th30;

    end;

    theorem :: YELLOW_0:33

    for L be complete antisymmetric non empty RelStr holds for a be Element of L, X be set holds a = ( "/\" (X,L)) iff a is_<=_than X & for b be Element of L st b is_<=_than X holds a >= b

    proof

      let L be complete non empty antisymmetric RelStr;

      let a be Element of L, X be set;

       ex_inf_of (X,L) by Th17;

      hence thesis by Th31;

    end;

    theorem :: YELLOW_0:34



     Th34: for L be RelStr, X,Y be set st X c= Y & ex_sup_of (X,L) & ex_sup_of (Y,L) holds ( "\/" (X,L)) <= ( "\/" (Y,L))

    proof

      let L be RelStr, X,Y be set;

      assume that

       A1: X c= Y and

       A2: ex_sup_of (X,L) and

       A3: ex_sup_of (Y,L);

      ( "\/" (Y,L)) is_>=_than X

      proof

        let x be Element of L;

        assume

         A4: x in X;

        ( "\/" (Y,L)) is_>=_than Y by A3, Def9;

        hence thesis by A1, A4;

      end;

      hence thesis by A2, Def9;

    end;

    theorem :: YELLOW_0:35



     Th35: for L be RelStr, X,Y be set st X c= Y & ex_inf_of (X,L) & ex_inf_of (Y,L) holds ( "/\" (X,L)) >= ( "/\" (Y,L))

    proof

      let L be RelStr, X,Y be set;

      assume that

       A1: X c= Y and

       A2: ex_inf_of (X,L) and

       A3: ex_inf_of (Y,L);

      ( "/\" (Y,L)) is_<=_than X

      proof

        let x be Element of L;

        assume

         A4: x in X;

        ( "/\" (Y,L)) is_<=_than Y by A3, Def10;

        hence thesis by A1, A4;

      end;

      hence thesis by A2, Def10;

    end;

    theorem :: YELLOW_0:36

    for L be antisymmetric transitive RelStr, X,Y be set st ex_sup_of (X,L) & ex_sup_of (Y,L) & ex_sup_of ((X \/ Y),L) holds ( "\/" ((X \/ Y),L)) = (( "\/" (X,L)) "\/" ( "\/" (Y,L)))

    proof

      let L be antisymmetric transitive RelStr;

      let X,Y be set such that

       A1: ex_sup_of (X,L) & ex_sup_of (Y,L) and

       A2: ex_sup_of ((X \/ Y),L);

      set a = ( "\/" (X,L)), b = ( "\/" (Y,L)), c = ( "\/" ((X \/ Y),L));



       A3: a is_>=_than X & b is_>=_than Y by A1, Th30;

       A4:

      now

        let d be Element of L;

        assume d >= a & d >= b;

        then d is_>=_than X & d is_>=_than Y by A3, Th4;

        then d is_>=_than (X \/ Y) by Th10;

        hence c <= d by A2, Th30;

      end;

      c >= a & c >= b by A1, A2, Th34, XBOOLE_1: 7;

      hence thesis by A4, Th18;

    end;

    theorem :: YELLOW_0:37

    for L be antisymmetric transitive RelStr, X,Y be set st ex_inf_of (X,L) & ex_inf_of (Y,L) & ex_inf_of ((X \/ Y),L) holds ( "/\" ((X \/ Y),L)) = (( "/\" (X,L)) "/\" ( "/\" (Y,L)))

    proof

      let L be antisymmetric transitive RelStr;

      let X,Y be set such that

       A1: ex_inf_of (X,L) & ex_inf_of (Y,L) and

       A2: ex_inf_of ((X \/ Y),L);

      set a = ( "/\" (X,L)), b = ( "/\" (Y,L)), c = ( "/\" ((X \/ Y),L));



       A3: a is_<=_than X & b is_<=_than Y by A1, Th31;

       A4:

      now

        let d be Element of L;

        assume d <= a & d <= b;

        then d is_<=_than X & d is_<=_than Y by A3, Th4;

        then d is_<=_than (X \/ Y) by Th10;

        hence c >= d by A2, Th31;

      end;

      c <= a & c <= b by A1, A2, Th35, XBOOLE_1: 7;

      hence thesis by A4, Th19;

    end;

    notation

      let L be RelStr;

      let X be Subset of L;

      synonym sup X for "\/" (X,L);

      synonym inf X for "/\" (X,L);

    end

    theorem :: YELLOW_0:38



     Th38: for L be non empty reflexive antisymmetric RelStr holds for a be Element of L holds ex_sup_of ( {a},L) & ex_inf_of ( {a},L)

    proof

      let L be non empty reflexive antisymmetric RelStr, a be Element of L;



       A1: for b be Element of L st b is_>=_than {a} holds b >= a by Th7;



       A2: a <= a;

      then a is_>=_than {a} by Th7;

      hence ex_sup_of ( {a},L) by A1, Th15;



       A3: for b be Element of L st b is_<=_than {a} holds b <= a by Th7;

      a is_<=_than {a} by A2, Th7;

      hence thesis by A3, Th16;

    end;

    theorem :: YELLOW_0:39

    for L be non empty reflexive antisymmetric RelStr holds for a be Element of L holds ( sup {a}) = a & ( inf {a}) = a

    proof

      let L be non empty reflexive antisymmetric RelStr;

      let a be Element of L;



       A1: for b be Element of L st b is_>=_than {a} holds b >= a by Th7;



       A2: a <= a;

      then a is_>=_than {a} by Th7;

      hence ( sup {a}) = a by A1, Th30;



       A3: for b be Element of L st b is_<=_than {a} holds b <= a by Th7;

      a is_<=_than {a} by A2, Th7;

      hence thesis by A3, Th31;

    end;

    theorem :: YELLOW_0:40



     Th40: for L be with_infima Poset, a,b be Element of L holds ( inf {a, b}) = (a "/\" b)

    proof

      let L be with_infima Poset, a,b be Element of L;

       A1:

      now

        let c be Element of L;

        assume c is_<=_than {a, b};

        then c <= a & c <= b by Th8;

        hence c <= (a "/\" b) by Th23;

      end;

      (a "/\" b) <= a & (a "/\" b) <= b by Th23;

      then

       A2: (a "/\" b) is_<=_than {a, b} by Th8;

      then ex_inf_of ( {a, b},L) by A1, Th16;

      hence thesis by A2, A1, Def10;

    end;

    theorem :: YELLOW_0:41



     Th41: for L be with_suprema Poset, a,b be Element of L holds ( sup {a, b}) = (a "\/" b)

    proof

      let L be with_suprema Poset, a,b be Element of L;

       A1:

      now

        let c be Element of L;

        assume c is_>=_than {a, b};

        then c >= a & c >= b by Th8;

        hence c >= (a "\/" b) by Th22;

      end;

      (a "\/" b) >= a & (a "\/" b) >= b by Th22;

      then

       A2: (a "\/" b) is_>=_than {a, b} by Th8;

      then ex_sup_of ( {a, b},L) by A1, Th15;

      hence thesis by A2, A1, Def9;

    end;

    theorem :: YELLOW_0:42



     Th42: for L be lower-bounded antisymmetric non empty RelStr holds ex_sup_of ( {} ,L) & ex_inf_of (the carrier of L,L)

    proof

      let L be lower-bounded antisymmetric non empty RelStr;

      consider a be Element of L such that

       A1: a is_<=_than the carrier of L by Def4;

      now

        take a;

        thus a is_>=_than {} ;

        thus for b be Element of L st b is_>=_than {} holds a <= b by A1;

      end;

      hence ex_sup_of ( {} ,L) by Th15;

      for b be Element of L st the carrier of L is_>=_than b holds a >= b;

      hence thesis by A1, Th16;

    end;

    theorem :: YELLOW_0:43



     Th43: for L be upper-bounded antisymmetric non empty RelStr holds ex_inf_of ( {} ,L) & ex_sup_of (the carrier of L,L)

    proof

      let L be upper-bounded antisymmetric non empty RelStr;

      consider a be Element of L such that

       A1: a is_>=_than the carrier of L by Def5;

      now

        take a;

        thus a is_<=_than {} ;

        thus for b be Element of L st b is_<=_than {} holds a >= b by A1;

      end;

      hence ex_inf_of ( {} ,L) by Th16;

      for b be Element of L st the carrier of L is_<=_than b holds a <= b;

      hence thesis by A1, Th15;

    end;

    definition

      let L be RelStr;

      :: YELLOW_0:def11

      func Bottom L -> Element of L equals ( "\/" ( {} ,L));

      correctness ;

      :: YELLOW_0:def12

      func Top L -> Element of L equals ( "/\" ( {} ,L));

      correctness ;

    end

    theorem :: YELLOW_0:44

    for L be lower-bounded antisymmetric non empty RelStr holds for x be Element of L holds ( Bottom L) <= x

    proof

      let L be lower-bounded antisymmetric non empty RelStr;

      let x be Element of L;

       {} is_<=_than x & ex_sup_of ( {} ,L) by Th42;

      hence thesis by Th30;

    end;

    theorem :: YELLOW_0:45

    for L be upper-bounded antisymmetric non empty RelStr holds for x be Element of L holds x <= ( Top L)

    proof

      let L be upper-bounded non empty antisymmetric RelStr;

      let x be Element of L;

       {} is_>=_than x & ex_inf_of ( {} ,L) by Th43;

      hence thesis by Th31;

    end;

    theorem :: YELLOW_0:46



     Th46: for L be non empty RelStr, X,Y be set st for x be Element of L holds x is_>=_than X iff x is_>=_than Y holds ex_sup_of (X,L) implies ex_sup_of (Y,L)

    proof

      let L be non empty RelStr, X,Y be set such that

       A1: for x be Element of L holds x is_>=_than X iff x is_>=_than Y;

      given a be Element of L such that

       A2: X is_<=_than a and

       A3: for b be Element of L st X is_<=_than b holds a <= b and

       A4: for c be Element of L st X is_<=_than c & for b be Element of L st X is_<=_than b holds c <= b holds c = a;

      take a;

      thus Y is_<=_than a by A1, A2;

      thus for b be Element of L st Y is_<=_than b holds a <= b by A1, A3;

      let c be Element of L;

      assume

       A5: Y is_<=_than c;

      assume

       A6: for b be Element of L st Y is_<=_than b holds c <= b;



       A7: for b be Element of L st X is_<=_than b holds c <= b by A1, A6;

      X is_<=_than c by A1, A5;

      hence thesis by A4, A7;

    end;

    theorem :: YELLOW_0:47



     Th47: for L be non empty RelStr, X,Y be set st ex_sup_of (X,L) & for x be Element of L holds x is_>=_than X iff x is_>=_than Y holds ( "\/" (X,L)) = ( "\/" (Y,L))

    proof

      let L be non empty RelStr, X,Y be set;

      assume

       A1: ex_sup_of (X,L);

      assume

       A2: for x be Element of L holds x is_>=_than X iff x is_>=_than Y;

       A3:

      now

        let b be Element of L;

        assume Y is_<=_than b;

        then X is_<=_than b by A2;

        hence ( "\/" (X,L)) <= b by A1, Def9;

      end;

      X is_<=_than ( "\/" (X,L)) by A1, Def9;

      then

       A4: Y is_<=_than ( "\/" (X,L)) by A2;

       ex_sup_of (Y,L) by A1, A2, Th46;

      hence thesis by A4, A3, Def9;

    end;

    theorem :: YELLOW_0:48



     Th48: for L be non empty RelStr, X,Y be set st for x be Element of L holds x is_<=_than X iff x is_<=_than Y holds ex_inf_of (X,L) implies ex_inf_of (Y,L)

    proof

      let L be non empty RelStr, X,Y be set such that

       A1: for x be Element of L holds x is_<=_than X iff x is_<=_than Y;

      given a be Element of L such that

       A2: X is_>=_than a and

       A3: for b be Element of L st X is_>=_than b holds a >= b and

       A4: for c be Element of L st X is_>=_than c & for b be Element of L st X is_>=_than b holds c >= b holds c = a;

      take a;

      thus Y is_>=_than a by A1, A2;

      thus for b be Element of L st Y is_>=_than b holds a >= b by A1, A3;

      let c be Element of L;

      assume

       A5: Y is_>=_than c;

      assume

       A6: for b be Element of L st Y is_>=_than b holds c >= b;



       A7: for b be Element of L st X is_>=_than b holds c >= b by A1, A6;

      X is_>=_than c by A1, A5;

      hence thesis by A4, A7;

    end;

    theorem :: YELLOW_0:49



     Th49: for L be non empty RelStr, X,Y be set st ex_inf_of (X,L) & for x be Element of L holds x is_<=_than X iff x is_<=_than Y holds ( "/\" (X,L)) = ( "/\" (Y,L))

    proof

      let L be non empty RelStr, X,Y be set;

      assume

       A1: ex_inf_of (X,L);

      assume

       A2: for x be Element of L holds x is_<=_than X iff x is_<=_than Y;

       A3:

      now

        let b be Element of L;

        assume Y is_>=_than b;

        then X is_>=_than b by A2;

        hence ( "/\" (X,L)) >= b by A1, Def10;

      end;

      X is_>=_than ( "/\" (X,L)) by A1, Def10;

      then

       A4: Y is_>=_than ( "/\" (X,L)) by A2;

       ex_inf_of (Y,L) by A1, A2, Th48;

      hence thesis by A4, A3, Def10;

    end;

    theorem :: YELLOW_0:50



     Th50: for L be non empty RelStr, X be set holds ( ex_sup_of (X,L) iff ex_sup_of ((X /\ the carrier of L),L)) & ( ex_inf_of (X,L) iff ex_inf_of ((X /\ the carrier of L),L))

    proof

      let L be non empty RelStr, X be set;

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

      (for x be Element of L holds x is_<=_than X iff x is_<=_than Y) & for x be Element of L holds x is_>=_than X iff x is_>=_than Y by Th5;

      hence thesis by Th46, Th48;

    end;

    theorem :: YELLOW_0:51

    for L be non empty RelStr, X be set st ex_sup_of (X,L) or ex_sup_of ((X /\ the carrier of L),L) holds ( "\/" (X,L)) = ( "\/" ((X /\ the carrier of L),L))

    proof

      let L be non empty RelStr, X be set;

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

      assume

       A1: ex_sup_of (X,L) or ex_sup_of (Y,L);

      for x be Element of L holds x is_>=_than X iff x is_>=_than Y by Th5;

      hence thesis by A1, Th47;

    end;

    theorem :: YELLOW_0:52

    for L be non empty RelStr, X be set st ex_inf_of (X,L) or ex_inf_of ((X /\ the carrier of L),L) holds ( "/\" (X,L)) = ( "/\" ((X /\ the carrier of L),L))

    proof

      let L be non empty RelStr, X be set;

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

      assume

       A1: ex_inf_of (X,L) or ex_inf_of (Y,L);

      for x be Element of L holds x is_<=_than X iff x is_<=_than Y by Th5;

      hence thesis by A1, Th49;

    end;

    theorem :: YELLOW_0:53

    for L be non empty RelStr st for X be Subset of L holds ex_sup_of (X,L) holds L is complete

    proof

      let L be non empty RelStr such that

       A1: for X be Subset of L holds ex_sup_of (X,L);

      let X be set;

      take ( "\/" (X,L));

      reconsider Y = (X /\ the carrier of L) as Subset of L by XBOOLE_1: 17;

       ex_sup_of (Y,L) by A1;

      then ex_sup_of (X,L) by Th50;

      hence thesis by Def9;

    end;

    theorem :: YELLOW_0:54

    for L be non empty Poset holds L is with_suprema iff for X be finite non empty Subset of L holds ex_sup_of (X,L)

    proof

      let L be non empty Poset;

      hereby

        defpred P[ set] means $1 is non empty implies ex_sup_of ($1,L);

        assume

         A1: L is with_suprema;

        let X be finite non empty Subset of L;



         A2: for x,Y be set st x in X & Y c= X & P[Y] holds P[(Y \/ {x})]

        proof

          let x,Y be set such that

           A3: x in X and Y c= X and

           A4: Y is non empty implies ex_sup_of (Y,L);

          reconsider z = x as Element of L by A3;

          assume (Y \/ {x}) is non empty;

          per cases ;

            suppose Y is empty;

            then (Y \/ {x}) = {z};

            hence thesis by Th38;

          end;

            suppose

             A5: Y is non empty;

            thus ex_sup_of ((Y \/ {x}),L)

            proof

              take a = (( "\/" (Y,L)) "\/" z);



               A6: Y is_<=_than ( "\/" (Y,L)) by A4, Def9;



               A7: ex_sup_of ( {( "\/" (Y,L)), z},L) by A1, Th20;

              then z <= a by Th18;

              then

               A8: {x} is_<=_than a by Th7;

              ( "\/" (Y,L)) <= a by A7, Th18;

              then

               A9: Y is_<=_than a by A6, Th11;

              hence (Y \/ {x}) is_<=_than a by A8, Th10;

              hereby

                let b be Element of L;

                assume

                 A10: (Y \/ {x}) is_<=_than b;

                Y c= (Y \/ {x}) by XBOOLE_1: 7;

                then Y is_<=_than b by A10;

                then

                 A11: ( "\/" (Y,L)) <= b by A4, A5, Def9;

                z in {x} by TARSKI:def 1;

                then z in (Y \/ {x}) by XBOOLE_0:def 3;

                then z <= b by A10;

                hence b >= a by A7, A11, Th18;

              end;

              let c be Element of L such that

               A12: (Y \/ {x}) is_<=_than c and

               A13: for b be Element of L st (Y \/ {x}) is_<=_than b holds b >= c;

              Y c= (Y \/ {x}) by XBOOLE_1: 7;

              then Y is_<=_than c by A12;

              then

               A14: ( "\/" (Y,L)) <= c by A4, A5, Def9;

              z in {x} by TARSKI:def 1;

              then z in (Y \/ {x}) by XBOOLE_0:def 3;

              then z <= c by A12;

              then

               A15: c >= a by A7, A14, Th18;

              a >= c by A9, A8, A13, Th10;

              hence thesis by A15, ORDERS_2: 2;

            end;

          end;

        end;



         A16: P[ {} ];



         A17: X is finite;

         P[X] from FINSET_1:sch 2( A17, A16, A2);

        hence ex_sup_of (X,L);

      end;

      assume for X be finite non empty Subset of L holds ex_sup_of (X,L);

      then for a,b be Element of L holds ex_sup_of ( {a, b},L);

      hence thesis by Th20;

    end;

    theorem :: YELLOW_0:55

    for L be non empty Poset holds L is with_infima iff for X be finite non empty Subset of L holds ex_inf_of (X,L)

    proof

      let L be non empty Poset;

      hereby

        defpred P[ set] means $1 is non empty implies ex_inf_of ($1,L);

        assume

         A1: L is with_infima;

        let X be finite non empty Subset of L;



         A2: for x,Y be set st x in X & Y c= X & P[Y] holds P[(Y \/ {x})]

        proof

          let x,Y be set such that

           A3: x in X and Y c= X and

           A4: Y is non empty implies ex_inf_of (Y,L);

          reconsider z = x as Element of L by A3;

          assume (Y \/ {x}) is non empty;

          per cases ;

            suppose Y is empty;

            then (Y \/ {x}) = {z};

            hence thesis by Th38;

          end;

            suppose

             A5: Y is non empty;

            thus ex_inf_of ((Y \/ {x}),L)

            proof

              take a = (( "/\" (Y,L)) "/\" z);



               A6: Y is_>=_than ( "/\" (Y,L)) by A4, Def10;



               A7: ex_inf_of ( {( "/\" (Y,L)), z},L) by A1, Th21;

              then z >= a by Th19;

              then

               A8: {x} is_>=_than a by Th7;

              ( "/\" (Y,L)) >= a by A7, Th19;

              then

               A9: Y is_>=_than a by A6, Th12;

              hence (Y \/ {x}) is_>=_than a by A8, Th10;

              hereby

                let b be Element of L;

                assume

                 A10: (Y \/ {x}) is_>=_than b;

                Y c= (Y \/ {x}) by XBOOLE_1: 7;

                then Y is_>=_than b by A10;

                then

                 A11: ( "/\" (Y,L)) >= b by A4, A5, Def10;

                z in {x} by TARSKI:def 1;

                then z in (Y \/ {x}) by XBOOLE_0:def 3;

                then z >= b by A10;

                hence b <= a by A7, A11, Th19;

              end;

              let c be Element of L such that

               A12: (Y \/ {x}) is_>=_than c and

               A13: for b be Element of L st (Y \/ {x}) is_>=_than b holds b <= c;

              Y c= (Y \/ {x}) by XBOOLE_1: 7;

              then Y is_>=_than c by A12;

              then

               A14: ( "/\" (Y,L)) >= c by A4, A5, Def10;

              z in {x} by TARSKI:def 1;

              then z in (Y \/ {x}) by XBOOLE_0:def 3;

              then z >= c by A12;

              then

               A15: c <= a by A7, A14, Th19;

              a <= c by A9, A8, A13, Th10;

              hence thesis by A15, ORDERS_2: 2;

            end;

          end;

        end;



         A16: P[ {} ];



         A17: X is finite;

         P[X] from FINSET_1:sch 2( A17, A16, A2);

        hence ex_inf_of (X,L);

      end;

      assume for X be finite non empty Subset of L holds ex_inf_of (X,L);

      then for a,b be Element of L holds ex_inf_of ( {a, b},L);

      hence thesis by Th21;

    end;

    begin

    definition

      let L be RelStr;

      :: YELLOW_0:def13

      mode SubRelStr of L -> RelStr means

      : Def13: the carrier of it c= the carrier of L & the InternalRel of it c= the InternalRel of L;

      existence ;

    end

    definition

      let L be RelStr;

      let S be SubRelStr of L;

      :: YELLOW_0:def14

      attr S is full means

      : Def14: the InternalRel of S = (the InternalRel of L |_2 the carrier of S);

    end

    registration

      let L be RelStr;

      cluster strict full for SubRelStr of L;

      existence

      proof

        set S = RelStr (# the carrier of L, the InternalRel of L #);

        reconsider S as SubRelStr of L by Def13;

        take S;

        thus S is strict;

        thus the InternalRel of S = (the InternalRel of L |_2 the carrier of S) by XBOOLE_1: 28;

      end;

    end

    registration

      let L be non empty RelStr;

      cluster non empty full strict for SubRelStr of L;

      existence

      proof

        set S = RelStr (# the carrier of L, the InternalRel of L #);

        reconsider S as SubRelStr of L by Def13;

        take S;

        thus the carrier of S is non empty;

        thus the InternalRel of S = (the InternalRel of L |_2 the carrier of S) by XBOOLE_1: 28;

        thus thesis;

      end;

    end

    theorem :: YELLOW_0:56



     Th56: for L be RelStr, X be Subset of L holds RelStr (# X, (the InternalRel of L |_2 X) #) is full SubRelStr of L by XBOOLE_1: 17, Def13, Def14;

    theorem :: YELLOW_0:57



     Th57: for L be RelStr, S1,S2 be full SubRelStr of L st the carrier of S1 = the carrier of S2 holds the RelStr of S1 = the RelStr of S2

    proof

      let L be RelStr, S1,S2 be full SubRelStr of L;

      the InternalRel of S1 = (the InternalRel of L |_2 the carrier of S1) by Def14;

      hence thesis by Def14;

    end;

    definition

      let L be RelStr;

      let X be Subset of L;

      :: YELLOW_0:def15

      func subrelstr X -> full strict SubRelStr of L means the carrier of it = X;

      uniqueness by Th57;

      existence

      proof

         RelStr (# X, (the InternalRel of L |_2 X) #) is full SubRelStr of L by Th56;

        hence thesis;

      end;

    end

    theorem :: YELLOW_0:58



     Th58: for L be non empty RelStr, S be non empty SubRelStr of L holds for x be Element of S holds x is Element of L

    proof

      let L be non empty RelStr, S be non empty SubRelStr of L;

      let x be Element of S;

      x in the carrier of S & the carrier of S c= the carrier of L by Def13;

      hence thesis;

    end;

    theorem :: YELLOW_0:59



     Th59: for L be RelStr, S be SubRelStr of L holds for a,b be Element of L holds for x,y be Element of S st x = a & y = b & x <= y holds a <= b

    proof

      let L be RelStr, S be SubRelStr of L;

      let a,b be Element of L, x,y be Element of S such that

       A1: x = a & y = b;



       A2: the InternalRel of S c= the InternalRel of L by Def13;

      assume [x, y] in the InternalRel of S;

      hence [a, b] in the InternalRel of L by A1, A2;

    end;

    theorem :: YELLOW_0:60



     Th60: for L be RelStr, S be full SubRelStr of L holds for a,b be Element of L holds for x,y be Element of S st x = a & y = b & a <= b & x in the carrier of S holds x <= y

    proof

      let L be RelStr, S be full SubRelStr of L;

      let a,b be Element of L, x,y be Element of S such that

       A1: x = a & y = b;

      assume

       A2: [a, b] in the InternalRel of L;



       A3: the InternalRel of S = (the InternalRel of L |_2 the carrier of S) by Def14;

      assume x in the carrier of S;

      then [x, y] in [:the carrier of S, the carrier of S:] by ZFMISC_1: 87;

      hence [x, y] in the InternalRel of S by A1, A3, A2, XBOOLE_0:def 4;

    end;

    theorem :: YELLOW_0:61



     Th61: for L be non empty RelStr, S be non empty full SubRelStr of L holds for X be set, a be Element of L holds for x be Element of S st x = a holds (a is_<=_than X implies x is_<=_than X) & (a is_>=_than X implies x is_>=_than X)

    proof

      let L be non empty RelStr, S be non empty full SubRelStr of L, X be set;

      let a be Element of L;

      let x be Element of S;

      assume

       A1: x = a;

      hereby

        assume

         A2: a is_<=_than X;

        thus x is_<=_than X

        proof

          let y be Element of S;

          reconsider b = y as Element of L by Th58;

          assume y in X;

          then a <= b by A2;

          hence thesis by A1, Th60;

        end;

      end;

      assume

       A3: a is_>=_than X;

      let y be Element of S;

      reconsider b = y as Element of L by Th58;

      assume y in X;

      then a >= b by A3;

      hence thesis by A1, Th60;

    end;

    theorem :: YELLOW_0:62



     Th62: for L be non empty RelStr, S be non empty SubRelStr of L holds for X be Subset of S holds for a be Element of L holds for x be Element of S st x = a holds (x is_<=_than X implies a is_<=_than X) & (x is_>=_than X implies a is_>=_than X) by Th59;

    registration

      let L be reflexive RelStr;

      cluster -> reflexive for full SubRelStr of L;

      coherence

      proof

        let S be full SubRelStr of L;

        let x be object;

        assume

         A1: x in the carrier of S;

        then

         A2: [x, x] in [:the carrier of S, the carrier of S:] by ZFMISC_1: 87;

        the carrier of S c= the carrier of L & the InternalRel of L is_reflexive_in the carrier of L by Def13, ORDERS_2:def 2;

        then

         A3: [x, x] in the InternalRel of L by A1;

        the InternalRel of S = (the InternalRel of L |_2 the carrier of S) by Def14;

        hence thesis by A2, A3, XBOOLE_0:def 4;

      end;

    end

    registration

      let L be transitive RelStr;

      cluster -> transitive for full SubRelStr of L;

      coherence

      proof

        let S be full SubRelStr of L;

        let x,y,z be Element of S;

        assume that

         A1: x <= y and

         A2: y <= z;



         A3: the carrier of S c= the carrier of L by Def13;

         [y, z] in the InternalRel of S by A2;

        then

         A4: z in the carrier of S by ZFMISC_1: 87;



         A5: [x, y] in the InternalRel of S by A1;

        then

         A6: x in the carrier of S by ZFMISC_1: 87;

        y in the carrier of S by A5, ZFMISC_1: 87;

        then

        reconsider a = x, b = y, c = z as Element of L by A6, A4, A3;

        a <= b & b <= c by A1, A2, Th59;

        hence thesis by A6, Th60, ORDERS_2: 3;

      end;

    end

    registration

      let L be antisymmetric RelStr;

      cluster -> antisymmetric for full SubRelStr of L;

      coherence

      proof

        let S be full SubRelStr of L;

        let x,y be Element of S;

        assume that

         A1: x <= y and

         A2: y <= x;



         A3: the carrier of S c= the carrier of L by Def13;

         [x, y] in the InternalRel of S by A1;

        then x in the carrier of S & y in the carrier of S by ZFMISC_1: 87;

        then

        reconsider a = x, b = y as Element of L by A3;

        a <= b & b <= a by A1, A2, Th59;

        hence thesis by ORDERS_2: 2;

      end;

    end

    definition

      let L be non empty RelStr;

      let S be SubRelStr of L;

      :: YELLOW_0:def16

      attr S is meet-inheriting means

      : Def16: 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;

      :: YELLOW_0:def17

      attr S is join-inheriting means

      : Def17: 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;

    end

    definition

      let L be non empty RelStr;

      let S be SubRelStr of L;

      :: YELLOW_0:def18

      attr S is infs-inheriting means for X be Subset of S st ex_inf_of (X,L) holds ( "/\" (X,L)) in the carrier of S;

      :: YELLOW_0:def19

      attr S is sups-inheriting means for X be Subset of S st ex_sup_of (X,L) holds ( "\/" (X,L)) in the carrier of S;

    end

    registration

      let L be non empty RelStr;

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

      coherence

      proof

        let S be SubRelStr of L;

        assume

         A1: for X be Subset of S st ex_inf_of (X,L) holds ( "/\" (X,L)) in the carrier of S;

        let x,y be Element of L;

        assume x in the carrier of S & y in the carrier of S;

        then {x, y} c= the carrier of S by ZFMISC_1: 32;

        hence thesis by A1;

      end;

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

      coherence

      proof

        let S be SubRelStr of L;

        assume

         A2: for X be Subset of S st ex_sup_of (X,L) holds ( "\/" (X,L)) in the carrier of S;

        let x,y be Element of L;

        assume x in the carrier of S & y in the carrier of S;

        then {x, y} c= the carrier of S by ZFMISC_1: 32;

        hence thesis by A2;

      end;

    end

    registration

      let L be non empty RelStr;

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

      existence

      proof

        the carrier of L c= the carrier of L & (the InternalRel of L |_2 the carrier of L) = the InternalRel of L by XBOOLE_1: 28;

        then

        reconsider S = RelStr (# the carrier of L, the InternalRel of L #) as non empty full strict SubRelStr of L by Th56;

        take S;

        thus S is infs-inheriting;

        thus S is sups-inheriting;

        thus thesis;

      end;

    end

    theorem :: YELLOW_0:63



     Th63: for L be non empty transitive RelStr holds for S be non empty full SubRelStr of L holds for X be Subset of S st ex_inf_of (X,L) & ( "/\" (X,L)) in the carrier of S holds ex_inf_of (X,S) & ( "/\" (X,S)) = ( "/\" (X,L))

    proof

      let L be non empty transitive RelStr;

      let S be non empty full SubRelStr of L;

      let X be Subset of S;

      assume that

       A1: ex_inf_of (X,L) and

       A2: ( "/\" (X,L)) in the carrier of S;

      reconsider a = ( "/\" (X,L)) as Element of S by A2;

       A3:

      now

        ( "/\" (X,L)) is_<=_than X by A1, Def10;

        hence a is_<=_than X by Th61;

        let b be Element of S;

        reconsider b9 = b as Element of L by Th58;

        assume b is_<=_than X;

        then b9 is_<=_than X by Th62;

        then b9 <= ( "/\" (X,L)) by A1, Def10;

        hence b <= a by Th60;

      end;

      consider a9 be Element of L such that

       A4: X is_>=_than a9 and

       A5: for b be Element of L st X is_>=_than b holds b <= a9 and 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 = a9 by A1;



       A6: a9 = ( "/\" (X,L)) by A1, A4, A5, Def10;

      thus ex_inf_of (X,S)

      proof

        take a;

        thus a is_<=_than X & for b be Element of S st b is_<=_than X holds b <= a by A3;

        let c be Element of S;

        reconsider c9 = c as Element of L by Th58;

        assume X is_>=_than c;

        then

         A7: X is_>=_than c9 by Th62;

        assume for b be Element of S st X is_>=_than b holds b <= c;

        then

         A8: a <= c by A3;

        now

          let b be Element of L;

          assume X is_>=_than b;

          then

           A9: b <= a9 by A5;

          a9 <= c9 by A6, A8, Th59;

          hence b <= c9 by A9, ORDERS_2: 3;

        end;

        hence thesis by A1, A7, Def10;

      end;

      hence thesis by A3, Def10;

    end;

    theorem :: YELLOW_0:64



     Th64: for L be non empty transitive RelStr holds for S be non empty full SubRelStr of L holds for X be Subset of S st ex_sup_of (X,L) & ( "\/" (X,L)) in the carrier of S holds ex_sup_of (X,S) & ( "\/" (X,S)) = ( "\/" (X,L))

    proof

      let L be non empty transitive RelStr;

      let S be non empty full SubRelStr of L;

      let X be Subset of S;

      assume that

       A1: ex_sup_of (X,L) and

       A2: ( "\/" (X,L)) in the carrier of S;

      reconsider a = ( "\/" (X,L)) as Element of S by A2;

       A3:

      now

        ( "\/" (X,L)) is_>=_than X by A1, Def9;

        hence a is_>=_than X by Th61;

        let b be Element of S;

        reconsider b9 = b as Element of L by Th58;

        assume b is_>=_than X;

        then b9 is_>=_than X by Th62;

        then b9 >= ( "\/" (X,L)) by A1, Def9;

        hence b >= a by Th60;

      end;

      consider a9 be Element of L such that

       A4: X is_<=_than a9 and

       A5: for b be Element of L st X is_<=_than b holds b >= a9 and 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 = a9 by A1;



       A6: a9 = ( "\/" (X,L)) by A1, A4, A5, Def9;

      thus ex_sup_of (X,S)

      proof

        take a;

        thus a is_>=_than X & for b be Element of S st b is_>=_than X holds b >= a by A3;

        let c be Element of S;

        reconsider c9 = c as Element of L by Th58;

        assume X is_<=_than c;

        then

         A7: X is_<=_than c9 by Th62;

        assume for b be Element of S st X is_<=_than b holds b >= c;

        then

         A8: a >= c by A3;

        now

          let b be Element of L;

          assume X is_<=_than b;

          then

           A9: b >= a9 by A5;

          a9 >= c9 by A6, A8, Th59;

          hence b >= c9 by A9, ORDERS_2: 3;

        end;

        hence thesis by A1, A7, Def9;

      end;

      hence thesis by A3, Def9;

    end;

    theorem :: YELLOW_0:65

    for L be non empty transitive RelStr holds for S be non empty full SubRelStr of L holds for x,y be Element of S st ex_inf_of ( {x, y},L) & ( "/\" ( {x, y},L)) in the carrier of S holds ex_inf_of ( {x, y},S) & ( "/\" ( {x, y},S)) = ( "/\" ( {x, y},L)) by Th63;

    theorem :: YELLOW_0:66

    for L be non empty transitive RelStr holds for S be non empty full SubRelStr of L holds for x,y be Element of S st ex_sup_of ( {x, y},L) & ( "\/" ( {x, y},L)) in the carrier of S holds ex_sup_of ( {x, y},S) & ( "\/" ( {x, y},S)) = ( "\/" ( {x, y},L)) by Th64;

    registration

      let L be with_infima antisymmetric transitive RelStr;

      cluster -> with_infima for non empty meet-inheriting full SubRelStr of L;

      coherence

      proof

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

        now

          let x,y be Element of S;

          reconsider a = x, b = y as Element of L by Th58;



           A1: ex_inf_of ( {a, b},L) by Th21;

          then ( "/\" ( {a, b},L)) in the carrier of S by Def16;

          hence ex_inf_of ( {x, y},S) by A1, Th63;

        end;

        hence thesis by Th21;

      end;

    end

    registration

      let L be with_suprema antisymmetric transitive RelStr;

      cluster -> with_suprema for non empty join-inheriting full SubRelStr of L;

      coherence

      proof

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

        now

          let x,y be Element of S;

          reconsider a = x, b = y as Element of L by Th58;



           A1: ex_sup_of ( {a, b},L) by Th20;

          then ( "\/" ( {a, b},L)) in the carrier of S by Def17;

          hence ex_sup_of ( {x, y},S) by A1, Th64;

        end;

        hence thesis by Th20;

      end;

    end

    theorem :: YELLOW_0:67

    for L be complete non empty Poset holds for S be non empty full SubRelStr of L holds for X be Subset of S st ( "/\" (X,L)) in the carrier of S holds ( "/\" (X,S)) = ( "/\" (X,L))

    proof

      let L be complete non empty Poset;

      let S be non empty full SubRelStr of L;

      let X be Subset of S such that

       A1: ( "/\" (X,L)) in the carrier of S;

       ex_inf_of (X,L) by Th17;

      hence thesis by A1, Th63;

    end;

    theorem :: YELLOW_0:68

    for L be complete non empty Poset holds for S be non empty full SubRelStr of L holds for X be Subset of S st ( "\/" (X,L)) in the carrier of S holds ( "\/" (X,S)) = ( "\/" (X,L))

    proof

      let L be complete non empty Poset;

      let S be non empty full SubRelStr of L;

      let X be Subset of S such that

       A1: ( "\/" (X,L)) in the carrier of S;

       ex_sup_of (X,L) by Th17;

      hence thesis by A1, Th64;

    end;

    theorem :: YELLOW_0:69

    for L be with_infima Poset holds for S be meet-inheriting non empty full SubRelStr of L holds for x,y be Element of S, a,b be Element of L st a = x & b = y holds (x "/\" y) = (a "/\" b)

    proof

      let L be with_infima Poset;

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

      let x,y be Element of S, a,b be Element of L such that

       A1: a = x & b = y;



       A2: ex_inf_of ( {a, b},L) by Th21;

      then ( "/\" ( {x, y},L)) in the carrier of S by A1, Def16;

      then

       A3: ( "/\" ( {x, y},S)) = ( "/\" ( {x, y},L)) by A1, A2, Th63;

      (a "/\" b) = ( inf {a, b}) by Th40;

      hence thesis by A1, A3, Th40;

    end;

    theorem :: YELLOW_0:70

    for L be with_suprema Poset holds for S be join-inheriting non empty full SubRelStr of L holds for x,y be Element of S, a,b be Element of L st a = x & b = y holds (x "\/" y) = (a "\/" b)

    proof

      let L be with_suprema Poset;

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

      let x,y be Element of S, a,b be Element of L such that

       A1: a = x & b = y;



       A2: ex_sup_of ( {a, b},L) by Th20;

      then ( "\/" ( {x, y},L)) in the carrier of S by A1, Def17;

      then

       A3: ( "\/" ( {x, y},S)) = ( "\/" ( {x, y},L)) by A1, A2, Th64;

      (a "\/" b) = ( sup {a, b}) by Th41;

      hence thesis by A1, A3, Th41;

    end;