yellow_4.miz

    begin

    theorem :: YELLOW_4:1



     Th1: for L be RelStr, X be set, a be Element of L st a in X & ex_sup_of (X,L) holds a <= ( "\/" (X,L))

    proof

      let L be RelStr, X be set, a be Element of L such that

       A1: a in X and

       A2: ex_sup_of (X,L);

      X is_<=_than ( "\/" (X,L)) by A2, YELLOW_0:def 9;

      hence thesis by A1;

    end;

    theorem :: YELLOW_4:2



     Th2: for L be RelStr, X be set, a be Element of L st a in X & ex_inf_of (X,L) holds ( "/\" (X,L)) <= a

    proof

      let L be RelStr, X be set, a be Element of L such that

       A1: a in X and

       A2: ex_inf_of (X,L);

      X is_>=_than ( "/\" (X,L)) by A2, YELLOW_0:def 10;

      hence thesis by A1;

    end;

    definition

      let L be RelStr, A,B be Subset of L;

      :: YELLOW_4:def1

      pred A is_finer_than B means for a be Element of L st a in A holds ex b be Element of L st b in B & a <= b;

      :: YELLOW_4:def2

      pred B is_coarser_than A means for b be Element of L st b in B holds ex a be Element of L st a in A & a <= b;

    end

    definition

      let L be non empty reflexive RelStr, A,B be Subset of L;

      :: original: is_finer_than

      redefine

      pred A is_finer_than B;

      reflexivity

      proof

        let A be Subset of L;

        let a be Element of L such that

         A1: a in A;

        take b = a;

        thus b in A & a <= b by A1;

      end;

      :: original: is_coarser_than

      redefine

      pred B is_coarser_than A;

      reflexivity

      proof

        let A be Subset of L;

        let a be Element of L such that

         A2: a in A;

        take b = a;

        thus b in A & b <= a by A2;

      end;

    end

    theorem :: YELLOW_4:3

    for L be RelStr, B be Subset of L holds ( {} L) is_finer_than B;

    theorem :: YELLOW_4:4

    for L be transitive RelStr, A,B,C be Subset of L st A is_finer_than B & B is_finer_than C holds A is_finer_than C

    proof

      let L be transitive RelStr, A,B,C be Subset of L such that

       A1: A is_finer_than B and

       A2: B is_finer_than C;

      let a be Element of L;

      assume a in A;

      then

      consider b be Element of L such that

       A3: b in B and

       A4: a <= b by A1;

      consider c be Element of L such that

       A5: c in C & b <= c by A2, A3;

      take c;

      thus thesis by A4, A5, ORDERS_2: 3;

    end;

    theorem :: YELLOW_4:5

    for L be RelStr, A,B be Subset of L st B is_finer_than A & A is lower holds B c= A

    proof

      let L be RelStr, A,B be Subset of L such that

       A1: B is_finer_than A and

       A2: A is lower;

      let a be object;

      assume

       A3: a in B;

      then

      reconsider a1 = a as Element of L;

      ex b be Element of L st b in A & a1 <= b by A1, A3;

      hence thesis by A2;

    end;

    theorem :: YELLOW_4:6

    for L be RelStr, A be Subset of L holds ( {} L) is_coarser_than A;

    theorem :: YELLOW_4:7

    for L be transitive RelStr, A,B,C be Subset of L st C is_coarser_than B & B is_coarser_than A holds C is_coarser_than A

    proof

      let L be transitive RelStr, A,B,C be Subset of L such that

       A1: C is_coarser_than B and

       A2: B is_coarser_than A;

      let c be Element of L;

      assume c in C;

      then

      consider b be Element of L such that

       A3: b in B and

       A4: b <= c by A1;

      consider a be Element of L such that

       A5: a in A & a <= b by A2, A3;

      take a;

      thus thesis by A4, A5, ORDERS_2: 3;

    end;

    theorem :: YELLOW_4:8

    for L be RelStr, A,B be Subset of L st A is_coarser_than B & B is upper holds A c= B

    proof

      let L be RelStr, A,B be Subset of L such that

       A1: A is_coarser_than B and

       A2: B is upper;

      let a be object;

      assume

       A3: a in A;

      then

      reconsider a1 = a as Element of L;

      ex b be Element of L st b in B & b <= a1 by A1, A3;

      hence thesis by A2;

    end;

    begin

    definition

      let L be non empty RelStr, D1,D2 be Subset of L;

      :: YELLOW_4:def3

      func D1 "\/" D2 -> Subset of L equals { (x "\/" y) where x,y be Element of L : x in D1 & y in D2 };

      coherence

      proof

        { (x "\/" y) where x,y be Element of L : x in D1 & y in D2 } c= the carrier of L

        proof

          let q be object;

          assume q in { (x "\/" y) where x,y be Element of L : x in D1 & y in D2 };

          then ex a,b be Element of L st q = (a "\/" b) & a in D1 & b in D2;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let L be with_suprema antisymmetric RelStr, D1,D2 be Subset of L;

      :: original: "\/"

      redefine

      func D1 "\/" D2;

      commutativity

      proof

        let D1,D2 be Subset of L;

        thus (D1 "\/" D2) c= (D2 "\/" D1)

        proof

          let q be object;

          assume q in (D1 "\/" D2);

          then ex x,y be Element of L st q = (x "\/" y) & x in D1 & y in D2;

          hence thesis;

        end;

        let q be object;

        assume q in (D2 "\/" D1);

        then ex x,y be Element of L st q = (x "\/" y) & x in D2 & y in D1;

        hence thesis;

      end;

    end

    theorem :: YELLOW_4:9

    for L be non empty RelStr, X be Subset of L holds (X "\/" ( {} L)) = {}

    proof

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

      thus (X "\/" ( {} L)) c= {}

      proof

        let a be object;

        assume a in (X "\/" ( {} L));

        then ex s,t be Element of L st a = (s "\/" t) & s in X & t in ( {} L);

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: YELLOW_4:10

    for L be non empty RelStr, X,Y be Subset of L, x,y be Element of L st x in X & y in Y holds (x "\/" y) in (X "\/" Y);

    theorem :: YELLOW_4:11

    for L be antisymmetric with_suprema RelStr holds for A be Subset of L, B be non empty Subset of L holds A is_finer_than (A "\/" B)

    proof

      let L be antisymmetric with_suprema RelStr, A be Subset of L, B be non empty Subset of L;

      let q be Element of L such that

       A1: q in A;

      set b = the Element of B;

      take (q "\/" b);

      thus (q "\/" b) in (A "\/" B) by A1;

      thus thesis by YELLOW_0: 22;

    end;

    theorem :: YELLOW_4:12

    for L be antisymmetric with_suprema RelStr, A,B be Subset of L holds (A "\/" B) is_coarser_than A

    proof

      let L be antisymmetric with_suprema RelStr, A,B be Subset of L;

      let q be Element of L;

      assume q in (A "\/" B);

      then

      consider x,y be Element of L such that

       A1: q = (x "\/" y) and

       A2: x in A and y in B;

      take x;

      thus x in A by A2;

      thus thesis by A1, YELLOW_0: 22;

    end;

    theorem :: YELLOW_4:13

    for L be antisymmetric reflexive with_suprema RelStr holds for A be Subset of L holds A c= (A "\/" A)

    proof

      let L be antisymmetric reflexive with_suprema RelStr, A be Subset of L;

      let q be object;

      assume

       A1: q in A;

      then

      reconsider A1 = A as non empty Subset of L;

      reconsider q1 = q as Element of A1 by A1;

      q1 <= q1;

      then q1 = (q1 "\/" q1) by YELLOW_0: 24;

      hence thesis;

    end;

    theorem :: YELLOW_4:14

    for L be with_suprema antisymmetric transitive RelStr holds for D1,D2,D3 be Subset of L holds ((D1 "\/" D2) "\/" D3) = (D1 "\/" (D2 "\/" D3))

    proof

      let L be with_suprema antisymmetric transitive RelStr, D1,D2,D3 be Subset of L;

      thus ((D1 "\/" D2) "\/" D3) c= (D1 "\/" (D2 "\/" D3))

      proof

        let q be object;

        assume q in ((D1 "\/" D2) "\/" D3);

        then

        consider a1,b1 be Element of L such that

         A1: q = (a1 "\/" b1) and

         A2: a1 in (D1 "\/" D2) and

         A3: b1 in D3;

        consider a11,b11 be Element of L such that

         A4: a1 = (a11 "\/" b11) and

         A5: a11 in D1 and

         A6: b11 in D2 by A2;

        (b11 "\/" b1) in (D2 "\/" D3) & q = (a11 "\/" (b11 "\/" b1)) by A1, A3, A4, A6, LATTICE3: 14;

        hence thesis by A5;

      end;

      let q be object;

      assume q in (D1 "\/" (D2 "\/" D3));

      then

      consider a1,b1 be Element of L such that

       A7: q = (a1 "\/" b1) & a1 in D1 and

       A8: b1 in (D2 "\/" D3);

      consider a11,b11 be Element of L such that

       A9: b1 = (a11 "\/" b11) & a11 in D2 and

       A10: b11 in D3 by A8;

      (a1 "\/" a11) in (D1 "\/" D2) & q = ((a1 "\/" a11) "\/" b11) by A7, A9, LATTICE3: 14;

      hence thesis by A10;

    end;

    registration

      let L be non empty RelStr, D1,D2 be non empty Subset of L;

      cluster (D1 "\/" D2) -> non empty;

      coherence

      proof

        consider b be object such that

         A1: b in D2 by XBOOLE_0:def 1;

        reconsider b as Element of D2 by A1;

        consider a be object such that

         A2: a in D1 by XBOOLE_0:def 1;

        reconsider a as Element of D1 by A2;

        (a "\/" b) in { (x "\/" y) where x,y be Element of L : x in D1 & y in D2 };

        hence thesis;

      end;

    end

    registration

      let L be with_suprema transitive antisymmetric RelStr, D1,D2 be directed Subset of L;

      cluster (D1 "\/" D2) -> directed;

      coherence

      proof

        let a,b be Element of L;

        set X = (D1 "\/" D2);

        assume that

         A1: a in X and

         A2: b in X;

        consider x,y be Element of L such that

         A3: a = (x "\/" y) and

         A4: x in D1 and

         A5: y in D2 by A1;

        consider s,t be Element of L such that

         A6: b = (s "\/" t) and

         A7: s in D1 and

         A8: t in D2 by A2;

        consider z2 be Element of L such that

         A9: z2 in D2 and

         A10: y <= z2 & t <= z2 by A5, A8, WAYBEL_0:def 1;

        consider z1 be Element of L such that

         A11: z1 in D1 and

         A12: x <= z1 & s <= z1 by A4, A7, WAYBEL_0:def 1;

        take z = (z1 "\/" z2);

        thus z in X by A11, A9;

        thus thesis by A3, A6, A12, A10, YELLOW_3: 3;

      end;

    end

    registration

      let L be with_suprema transitive antisymmetric RelStr, D1,D2 be filtered Subset of L;

      cluster (D1 "\/" D2) -> filtered;

      coherence

      proof

        let a,b be Element of L;

        set X = (D1 "\/" D2);

        assume that

         A1: a in X and

         A2: b in X;

        consider x,y be Element of L such that

         A3: a = (x "\/" y) and

         A4: x in D1 and

         A5: y in D2 by A1;

        consider s,t be Element of L such that

         A6: b = (s "\/" t) and

         A7: s in D1 and

         A8: t in D2 by A2;

        consider z2 be Element of L such that

         A9: z2 in D2 and

         A10: y >= z2 & t >= z2 by A5, A8, WAYBEL_0:def 2;

        consider z1 be Element of L such that

         A11: z1 in D1 and

         A12: x >= z1 & s >= z1 by A4, A7, WAYBEL_0:def 2;

        take z = (z1 "\/" z2);

        thus z in X by A11, A9;

        thus thesis by A3, A6, A12, A10, YELLOW_3: 3;

      end;

    end

    registration

      let L be with_suprema Poset, D1,D2 be upper Subset of L;

      cluster (D1 "\/" D2) -> upper;

      coherence

      proof

        set X = (D1 "\/" D2);

        let a,b be Element of L such that

         A1: a in X and

         A2: a <= b;

        consider x,y be Element of L such that

         A3: a = (x "\/" y) and

         A4: x in D1 and

         A5: y in D2 by A1;



         A6: ex xx be Element of L st x <= xx & y <= xx & for c be Element of L st x <= c & y <= c holds xx <= c by LATTICE3:def 10;

        then x <= (x "\/" y) by LATTICE3:def 13;

        then x <= b by A2, A3, YELLOW_0:def 2;

        then

         A7: b in D1 by A4, WAYBEL_0:def 20;

        y <= (x "\/" y) by A6, LATTICE3:def 13;

        then y <= b by A2, A3, YELLOW_0:def 2;

        then

         A8: b in D2 by A5, WAYBEL_0:def 20;

        b <= b;

        then b = (b "\/" b) by YELLOW_0: 24;

        hence thesis by A7, A8;

      end;

    end

    theorem :: YELLOW_4:15



     Th15: for L be non empty RelStr, Y be Subset of L, x be Element of L holds ( {x} "\/" Y) = { (x "\/" y) where y be Element of L : y in Y }

    proof

      let L be non empty RelStr, Y be Subset of L, x be Element of L;

      thus ( {x} "\/" Y) c= { (x "\/" y) where y be Element of L : y in Y }

      proof

        let q be object;

        assume q in ( {x} "\/" Y);

        then

        consider s,t be Element of L such that

         A1: q = (s "\/" t) and

         A2: s in {x} and

         A3: t in Y;

        s = x by A2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let q be object;

      assume q in { (x "\/" y) where y be Element of L : y in Y };

      then

       A4: ex y be Element of L st q = (x "\/" y) & y in Y;

      x in {x} by TARSKI:def 1;

      hence thesis by A4;

    end;

    theorem :: YELLOW_4:16

    for L be non empty RelStr, A,B,C be Subset of L holds (A "\/" (B \/ C)) = ((A "\/" B) \/ (A "\/" C))

    proof

      let L be non empty RelStr, A,B,C be Subset of L;

      thus (A "\/" (B \/ C)) c= ((A "\/" B) \/ (A "\/" C))

      proof

        let q be object;

        assume q in (A "\/" (B \/ C));

        then

        consider a,y be Element of L such that

         A1: q = (a "\/" y) & a in A and

         A2: y in (B \/ C);

        y in B or y in C by A2, XBOOLE_0:def 3;

        then q in (A "\/" B) or q in (A "\/" C) by A1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let q be object such that

       A3: q in ((A "\/" B) \/ (A "\/" C));

      per cases by A3, XBOOLE_0:def 3;

        suppose q in (A "\/" B);

        then

        consider a,b be Element of L such that

         A4: q = (a "\/" b) & a in A and

         A5: b in B;

        b in (B \/ C) by A5, XBOOLE_0:def 3;

        hence thesis by A4;

      end;

        suppose q in (A "\/" C);

        then

        consider a,b be Element of L such that

         A6: q = (a "\/" b) & a in A and

         A7: b in C;

        b in (B \/ C) by A7, XBOOLE_0:def 3;

        hence thesis by A6;

      end;

    end;

    theorem :: YELLOW_4:17

    for L be antisymmetric reflexive with_suprema RelStr holds for A,B,C be Subset of L holds (A \/ (B "\/" C)) c= ((A \/ B) "\/" (A \/ C))

    proof

      let L be antisymmetric reflexive with_suprema RelStr, A,B,C be Subset of L;

      let q be object such that

       A1: q in (A \/ (B "\/" C));

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: q in A;

        then

        reconsider q1 = q as Element of L;

        q1 <= q1;

        then

         A3: q1 = (q1 "\/" q1) by YELLOW_0: 24;

        q1 in (A \/ B) & q1 in (A \/ C) by A2, XBOOLE_0:def 3;

        hence thesis by A3;

      end;

        suppose q in (B "\/" C);

        then

        consider b,c be Element of L such that

         A4: q = (b "\/" c) and

         A5: b in B & c in C;

        b in (A \/ B) & c in (A \/ C) by A5, XBOOLE_0:def 3;

        hence thesis by A4;

      end;

    end;

    theorem :: YELLOW_4:18

    for L be antisymmetric with_suprema RelStr, A be upper Subset of L holds for B,C be Subset of L holds ((A \/ B) "\/" (A \/ C)) c= (A \/ (B "\/" C))

    proof

      let L be antisymmetric with_suprema RelStr, A be upper Subset of L, B,C be Subset of L;

      let q be object;

      assume q in ((A \/ B) "\/" (A \/ C));

      then

      consider x,y be Element of L such that

       A1: q = (x "\/" y) and

       A2: x in (A \/ B) & y in (A \/ C);



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



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

      per cases by A2, XBOOLE_0:def 3;

        suppose x in A & y in A;

        then q in A by A1, A3, WAYBEL_0:def 20;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose x in A & y in C;

        then q in A by A1, A3, WAYBEL_0:def 20;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose x in B & y in A;

        then q in A by A1, A4, WAYBEL_0:def 20;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose x in B & y in C;

        then (x "\/" y) in (B "\/" C);

        hence thesis by A1, XBOOLE_0:def 3;

      end;

    end;

     Lm1:

    now

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

      thus { (a "\/" b) where a,b be Element of L : a in {x} & b in {y} } = {(x "\/" y)}

      proof

        thus { (a "\/" b) where a,b be Element of L : a in {x} & b in {y} } c= {(x "\/" y)}

        proof

          let q be object;

          assume q in { (a "\/" b) where a,b be Element of L : a in {x} & b in {y} };

          then

          consider u,v be Element of L such that

           A1: q = (u "\/" v) and

           A2: u in {x} & v in {y};

          u = x & v = y by A2, TARSKI:def 1;

          hence thesis by A1, TARSKI:def 1;

        end;

        let q be object;

        assume q in {(x "\/" y)};

        then

         A3: q = (x "\/" y) by TARSKI:def 1;

        x in {x} & y in {y} by TARSKI:def 1;

        hence thesis by A3;

      end;

    end;

     Lm2:

    now

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

      thus { (a "\/" b) where a,b be Element of L : a in {x} & b in {y, z} } = {(x "\/" y), (x "\/" z)}

      proof

        thus { (a "\/" b) where a,b be Element of L : a in {x} & b in {y, z} } c= {(x "\/" y), (x "\/" z)}

        proof

          let q be object;

          assume q in { (a "\/" b) where a,b be Element of L : a in {x} & b in {y, z} };

          then

          consider u,v be Element of L such that

           A1: q = (u "\/" v) and

           A2: u in {x} and

           A3: v in {y, z};



           A4: v = y or v = z by A3, TARSKI:def 2;

          u = x by A2, TARSKI:def 1;

          hence thesis by A1, A4, TARSKI:def 2;

        end;

        let q be object;



         A5: z in {y, z} by TARSKI:def 2;

        assume q in {(x "\/" y), (x "\/" z)};

        then

         A6: q = (x "\/" y) or q = (x "\/" z) by TARSKI:def 2;

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

        hence thesis by A6, A5;

      end;

    end;

    theorem :: YELLOW_4:19

    for L be non empty RelStr, x,y be Element of L holds ( {x} "\/" {y}) = {(x "\/" y)} by Lm1;

    theorem :: YELLOW_4:20

    for L be non empty RelStr, x,y,z be Element of L holds ( {x} "\/" {y, z}) = {(x "\/" y), (x "\/" z)} by Lm2;

    theorem :: YELLOW_4:21

    for L be non empty RelStr, X1,X2,Y1,Y2 be Subset of L st X1 c= Y1 & X2 c= Y2 holds (X1 "\/" X2) c= (Y1 "\/" Y2)

    proof

      let L be non empty RelStr, X1,X2,Y1,Y2 be Subset of L such that

       A1: X1 c= Y1 & X2 c= Y2;

      let q be object;

      assume q in (X1 "\/" X2);

      then ex x,y be Element of L st q = (x "\/" y) & x in X1 & y in X2;

      hence thesis by A1;

    end;

    theorem :: YELLOW_4:22

    for L be with_suprema reflexive antisymmetric RelStr holds for D be Subset of L, x be Element of L st x is_<=_than D holds ( {x} "\/" D) = D

    proof

      let L be with_suprema reflexive antisymmetric RelStr, D be Subset of L, x be Element of L such that

       A1: x is_<=_than D;



       A2: ( {x} "\/" D) = { (x "\/" y) where y be Element of L : y in D } by Th15;

      thus ( {x} "\/" D) c= D

      proof

        let q be object;

        assume q in ( {x} "\/" D);

        then

        consider y be Element of L such that

         A3: q = (x "\/" y) and

         A4: y in D by A2;

        x <= y by A1, A4;

        hence thesis by A3, A4, YELLOW_0: 24;

      end;

      let q be object;

      assume

       A5: q in D;

      then

      reconsider D1 = D as non empty Subset of L;

      reconsider y = q as Element of D1 by A5;

      x <= y by A1;

      then q = (x "\/" y) by YELLOW_0: 24;

      hence thesis by A2;

    end;

    theorem :: YELLOW_4:23

    for L be with_suprema antisymmetric RelStr holds for D be Subset of L, x be Element of L holds x is_<=_than ( {x} "\/" D)

    proof

      let L be with_suprema antisymmetric RelStr, D be Subset of L, x be Element of L;

      let b be Element of L;



       A1: ( {x} "\/" D) = { (x "\/" h) where h be Element of L : h in D } by Th15;

      assume b in ( {x} "\/" D);

      then

      consider h be Element of L such that

       A2: b = (x "\/" h) and h in D by A1;

      ex w be Element of L st x <= w & h <= w & for c be Element of L st x <= c & h <= c holds w <= c by LATTICE3:def 10;

      hence thesis by A2, LATTICE3:def 13;

    end;

    theorem :: YELLOW_4:24

    for L be with_suprema Poset, X be Subset of L, x be Element of L st ex_inf_of (( {x} "\/" X),L) & ex_inf_of (X,L) holds (x "\/" ( inf X)) <= ( inf ( {x} "\/" X))

    proof

      let L be with_suprema Poset, X be Subset of L, x be Element of L such that

       A1: ex_inf_of (( {x} "\/" X),L) and

       A2: ex_inf_of (X,L);



       A3: ( {x} "\/" X) = { (x "\/" y) where y be Element of L : y in X } by Th15;

      ( {x} "\/" X) is_>=_than (x "\/" ( inf X))

      proof

        let q be Element of L;

        assume q in ( {x} "\/" X);

        then

        consider y be Element of L such that

         A4: q = (x "\/" y) and

         A5: y in X by A3;

        x <= x & y >= ( inf X) by A2, A5, Th2;

        hence thesis by A4, YELLOW_3: 3;

      end;

      hence thesis by A1, YELLOW_0:def 10;

    end;

    theorem :: YELLOW_4:25



     Th25: for L be complete transitive antisymmetric non empty RelStr holds for A be Subset of L, B be non empty Subset of L holds A is_<=_than ( sup (A "\/" B))

    proof

      let L be complete transitive antisymmetric non empty RelStr, A be Subset of L, B be non empty Subset of L;

      set b = the Element of B;

      let x be Element of L;

      assume x in A;

      then

       A1: (x "\/" b) in (A "\/" B);

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

      then

       A2: x <= (x "\/" b) by LATTICE3:def 13;

       ex_sup_of ((A "\/" B),L) by YELLOW_0: 17;

      then (A "\/" B) is_<=_than ( sup (A "\/" B)) by YELLOW_0:def 9;

      then (x "\/" b) <= ( sup (A "\/" B)) by A1;

      hence thesis by A2, YELLOW_0:def 2;

    end;

    theorem :: YELLOW_4:26

    for L be with_suprema transitive antisymmetric RelStr holds for a,b be Element of L, A,B be Subset of L st a is_<=_than A & b is_<=_than B holds (a "\/" b) is_<=_than (A "\/" B)

    proof

      let L be with_suprema transitive antisymmetric RelStr, a,b be Element of L, A,B be Subset of L such that

       A1: a is_<=_than A & b is_<=_than B;

      let q be Element of L;

      assume q in (A "\/" B);

      then

      consider x,y be Element of L such that

       A2: q = (x "\/" y) and

       A3: x in A & y in B;

      a <= x & b <= y by A1, A3;

      hence thesis by A2, YELLOW_3: 3;

    end;

    theorem :: YELLOW_4:27



     Th27: for L be with_suprema transitive antisymmetric RelStr holds for a,b be Element of L, A,B be Subset of L st a is_>=_than A & b is_>=_than B holds (a "\/" b) is_>=_than (A "\/" B)

    proof

      let L be with_suprema transitive antisymmetric RelStr, a,b be Element of L, A,B be Subset of L such that

       A1: a is_>=_than A & b is_>=_than B;

      let q be Element of L;

      assume q in (A "\/" B);

      then

      consider x,y be Element of L such that

       A2: q = (x "\/" y) and

       A3: x in A & y in B;

      a >= x & b >= y by A1, A3;

      hence thesis by A2, YELLOW_3: 3;

    end;

    theorem :: YELLOW_4:28

    for L be complete non empty Poset holds for A,B be non empty Subset of L holds ( sup (A "\/" B)) = (( sup A) "\/" ( sup B))

    proof

      let L be complete non empty Poset, A,B be non empty Subset of L;

      B is_<=_than ( sup (A "\/" B)) by Th25;

      then

       A1: ( sup B) <= ( sup (A "\/" B)) by YELLOW_0: 32;

      A is_<=_than ( sup (A "\/" B)) by Th25;

      then ( sup A) <= ( sup (A "\/" B)) by YELLOW_0: 32;

      then

       A2: (( sup A) "\/" ( sup B)) <= (( sup (A "\/" B)) "\/" ( sup (A "\/" B))) by A1, YELLOW_3: 3;

      A is_<=_than ( sup A) & B is_<=_than ( sup B) by YELLOW_0: 32;

      then ex_sup_of ((A "\/" B),L) & (A "\/" B) is_<=_than (( sup A) "\/" ( sup B)) by Th27, YELLOW_0: 17;

      then

       A3: ( sup (A "\/" B)) <= (( sup A) "\/" ( sup B)) by YELLOW_0:def 9;

      ( sup (A "\/" B)) <= ( sup (A "\/" B));

      then (( sup (A "\/" B)) "\/" ( sup (A "\/" B))) = ( sup (A "\/" B)) by YELLOW_0: 24;

      hence thesis by A3, A2, ORDERS_2: 2;

    end;

    theorem :: YELLOW_4:29



     Th29: for L be with_suprema antisymmetric RelStr holds for X be Subset of L, Y be non empty Subset of L holds X c= ( downarrow (X "\/" Y))

    proof

      let L be with_suprema antisymmetric RelStr, X be Subset of L, Y be non empty Subset of L;

      consider y be object such that

       A1: y in Y by XBOOLE_0:def 1;

      reconsider y as Element of Y by A1;

      let q be object;

      assume

       A2: q in X;

      then

      reconsider X1 = X as non empty Subset of L;

      reconsider x = q as Element of X1 by A2;

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

      then

       A3: x <= (x "\/" y) by LATTICE3:def 13;

      ( downarrow (X "\/" Y)) = { s where s be Element of L : ex y be Element of L st s <= y & y in (X "\/" Y) } & (x "\/" y) in (X1 "\/" Y) by WAYBEL_0: 14;

      hence thesis by A3;

    end;

    theorem :: YELLOW_4:30

    for L be with_suprema Poset holds for x,y be Element of ( InclPoset ( Ids L)) holds for X,Y be Subset of L st x = X & y = Y holds (x "\/" y) = ( downarrow (X "\/" Y))

    proof

      let L be with_suprema Poset, x,y be Element of ( InclPoset ( Ids L)), X,Y be Subset of L such that

       A1: x = X and

       A2: y = Y;

      reconsider X1 = X, Y1 = Y as non empty directed Subset of L by A1, A2, YELLOW_2: 41;

      reconsider d = ( downarrow (X1 "\/" Y1)) as Element of ( InclPoset ( Ids L)) by YELLOW_2: 41;

      Y c= d by Th29;

      then

       A3: y <= d by A2, YELLOW_1: 3;

      X c= d by Th29;

      then x <= d by A1, YELLOW_1: 3;

      then d <= d & (x "\/" y) <= (d "\/" d) by A3, YELLOW_3: 3;

      then (x "\/" y) <= d by YELLOW_0: 24;

      hence (x "\/" y) c= ( downarrow (X "\/" Y)) by YELLOW_1: 3;

      consider Z be Subset of L such that

       A4: Z = { z where z be Element of L : z in x or z in y or ex a,b be Element of L st a in x & b in y & z = (a "\/" b) } and ex_sup_of ( {x, y},( InclPoset ( Ids L))) and

       A5: (x "\/" y) = ( downarrow Z) by YELLOW_2: 44;

      (X "\/" Y) c= Z

      proof

        let q be object;

        assume q in (X "\/" Y);

        then ex s,t be Element of L st q = (s "\/" t) & s in X & t in Y;

        hence thesis by A1, A2, A4;

      end;

      hence thesis by A5, YELLOW_3: 6;

    end;

    theorem :: YELLOW_4:31

    for L be non empty RelStr, D be Subset of [:L, L:] holds ( union { X where X be Subset of L : ex x be Element of L st X = ( {x} "\/" ( proj2 D)) & x in ( proj1 D) }) = (( proj1 D) "\/" ( proj2 D))

    proof

      let L be non empty RelStr, D be Subset of [:L, L:];

      set D1 = ( proj1 D), D2 = ( proj2 D);

      defpred P[ set] means ex x be Element of L st $1 = ( {x} "\/" ( proj2 D)) & x in ( proj1 D);

      thus ( union { X where X be Subset of L : P[X] }) c= (D1 "\/" D2)

      proof

        let q be object;

        assume q in ( union { X where X be Subset of L : P[X] });

        then

        consider w be set such that

         A1: q in w and

         A2: w in { X where X be Subset of L : P[X] } by TARSKI:def 4;

        consider e be Subset of L such that

         A3: w = e and

         A4: P[e] by A2;

        consider p be Element of L such that

         A5: e = ( {p} "\/" D2) and

         A6: p in D1 by A4;

        ( {p} "\/" D2) = { (p "\/" y) where y be Element of L : y in D2 } by Th15;

        then ex y be Element of L st q = (p "\/" y) & y in D2 by A1, A3, A5;

        hence thesis by A6;

      end;

      let q be object;

      assume q in (D1 "\/" D2);

      then

      consider x,y be Element of L such that

       A7: q = (x "\/" y) and

       A8: x in D1 and

       A9: y in D2;

      ( {x} "\/" D2) = { (x "\/" d) where d be Element of L : d in D2 } by Th15;

      then

       A10: q in ( {x} "\/" D2) by A7, A9;

      ( {x} "\/" D2) in { X where X be Subset of L : P[X] } by A8;

      hence thesis by A10, TARSKI:def 4;

    end;

    theorem :: YELLOW_4:32



     Th32: for L be transitive antisymmetric with_suprema RelStr holds for D1,D2 be Subset of L holds ( downarrow (( downarrow D1) "\/" ( downarrow D2))) c= ( downarrow (D1 "\/" D2))

    proof

      let L be transitive antisymmetric with_suprema RelStr, D1,D2 be Subset of L;



       A1: ( downarrow (( downarrow D1) "\/" ( downarrow D2))) = { x where x be Element of L : ex t be Element of L st x <= t & t in (( downarrow D1) "\/" ( downarrow D2)) } by WAYBEL_0: 14;

      let y be object;

      assume y in ( downarrow (( downarrow D1) "\/" ( downarrow D2)));

      then

      consider x be Element of L such that

       A2: y = x and

       A3: ex t be Element of L st x <= t & t in (( downarrow D1) "\/" ( downarrow D2)) by A1;

      consider x1 be Element of L such that

       A4: x <= x1 and

       A5: x1 in (( downarrow D1) "\/" ( downarrow D2)) by A3;

      consider a,b be Element of L such that

       A6: x1 = (a "\/" b) and

       A7: a in ( downarrow D1) and

       A8: b in ( downarrow D2) by A5;

      ( downarrow D2) = { s2 where s2 be Element of L : ex z be Element of L st s2 <= z & z in D2 } by WAYBEL_0: 14;

      then

      consider B1 be Element of L such that

       A9: b = B1 and

       A10: ex z be Element of L st B1 <= z & z in D2 by A8;

      consider b1 be Element of L such that

       A11: B1 <= b1 and

       A12: b1 in D2 by A10;

      ( downarrow D1) = { s1 where s1 be Element of L : ex z be Element of L st s1 <= z & z in D1 } by WAYBEL_0: 14;

      then

      consider A1 be Element of L such that

       A13: a = A1 and

       A14: ex z be Element of L st A1 <= z & z in D1 by A7;

      consider a1 be Element of L such that

       A15: A1 <= a1 and

       A16: a1 in D1 by A14;

      x1 <= (a1 "\/" b1) by A6, A13, A9, A15, A11, YELLOW_3: 3;

      then

       A17: ( downarrow (D1 "\/" D2)) = { s where s be Element of L : ex z be Element of L st s <= z & z in (D1 "\/" D2) } & x <= (a1 "\/" b1) by A4, ORDERS_2: 3, WAYBEL_0: 14;

      (a1 "\/" b1) in (D1 "\/" D2) by A16, A12;

      hence thesis by A2, A17;

    end;

    theorem :: YELLOW_4:33

    for L be with_suprema Poset, D1,D2 be Subset of L holds ( downarrow (( downarrow D1) "\/" ( downarrow D2))) = ( downarrow (D1 "\/" D2))

    proof

      let L be with_suprema Poset, D1,D2 be Subset of L;



       A1: ( downarrow (D1 "\/" D2)) = { s where s be Element of L : ex z be Element of L st s <= z & z in (D1 "\/" D2) } by WAYBEL_0: 14;

      thus ( downarrow (( downarrow D1) "\/" ( downarrow D2))) c= ( downarrow (D1 "\/" D2)) by Th32;

      let q be object;

      assume q in ( downarrow (D1 "\/" D2));

      then

      consider s be Element of L such that

       A2: q = s and

       A3: ex z be Element of L st s <= z & z in (D1 "\/" D2) by A1;



       A4: ( downarrow (( downarrow D1) "\/" ( downarrow D2))) = { x where x be Element of L : ex t be Element of L st x <= t & t in (( downarrow D1) "\/" ( downarrow D2)) } by WAYBEL_0: 14;



       A5: D1 is Subset of ( downarrow D1) & D2 is Subset of ( downarrow D2) by WAYBEL_0: 16;

      consider x be Element of L such that

       A6: s <= x and

       A7: x in (D1 "\/" D2) by A3;

      ex a,b be Element of L st x = (a "\/" b) & a in D1 & b in D2 by A7;

      then x in (( downarrow D1) "\/" ( downarrow D2)) by A5;

      hence thesis by A4, A2, A6;

    end;

    theorem :: YELLOW_4:34



     Th34: for L be transitive antisymmetric with_suprema RelStr holds for D1,D2 be Subset of L holds ( uparrow (( uparrow D1) "\/" ( uparrow D2))) c= ( uparrow (D1 "\/" D2))

    proof

      let L be transitive antisymmetric with_suprema RelStr, D1,D2 be Subset of L;



       A1: ( uparrow (( uparrow D1) "\/" ( uparrow D2))) = { x where x be Element of L : ex t be Element of L st x >= t & t in (( uparrow D1) "\/" ( uparrow D2)) } by WAYBEL_0: 15;

      let y be object;

      assume y in ( uparrow (( uparrow D1) "\/" ( uparrow D2)));

      then

      consider x be Element of L such that

       A2: y = x and

       A3: ex t be Element of L st x >= t & t in (( uparrow D1) "\/" ( uparrow D2)) by A1;

      consider x1 be Element of L such that

       A4: x >= x1 and

       A5: x1 in (( uparrow D1) "\/" ( uparrow D2)) by A3;

      consider a,b be Element of L such that

       A6: x1 = (a "\/" b) and

       A7: a in ( uparrow D1) and

       A8: b in ( uparrow D2) by A5;

      ( uparrow D2) = { s2 where s2 be Element of L : ex z be Element of L st s2 >= z & z in D2 } by WAYBEL_0: 15;

      then

      consider B1 be Element of L such that

       A9: b = B1 and

       A10: ex z be Element of L st B1 >= z & z in D2 by A8;

      consider b1 be Element of L such that

       A11: B1 >= b1 and

       A12: b1 in D2 by A10;

      ( uparrow D1) = { s1 where s1 be Element of L : ex z be Element of L st s1 >= z & z in D1 } by WAYBEL_0: 15;

      then

      consider A1 be Element of L such that

       A13: a = A1 and

       A14: ex z be Element of L st A1 >= z & z in D1 by A7;

      consider a1 be Element of L such that

       A15: A1 >= a1 and

       A16: a1 in D1 by A14;

      x1 >= (a1 "\/" b1) by A6, A13, A9, A15, A11, YELLOW_3: 3;

      then

       A17: ( uparrow (D1 "\/" D2)) = { s where s be Element of L : ex z be Element of L st s >= z & z in (D1 "\/" D2) } & x >= (a1 "\/" b1) by A4, ORDERS_2: 3, WAYBEL_0: 15;

      (a1 "\/" b1) in (D1 "\/" D2) by A16, A12;

      hence thesis by A2, A17;

    end;

    theorem :: YELLOW_4:35

    for L be with_suprema Poset, D1,D2 be Subset of L holds ( uparrow (( uparrow D1) "\/" ( uparrow D2))) = ( uparrow (D1 "\/" D2))

    proof

      let L be with_suprema Poset, D1,D2 be Subset of L;



       A1: ( uparrow (D1 "\/" D2)) = { s where s be Element of L : ex z be Element of L st s >= z & z in (D1 "\/" D2) } by WAYBEL_0: 15;

      thus ( uparrow (( uparrow D1) "\/" ( uparrow D2))) c= ( uparrow (D1 "\/" D2)) by Th34;

      let q be object;

      assume q in ( uparrow (D1 "\/" D2));

      then

      consider s be Element of L such that

       A2: q = s and

       A3: ex z be Element of L st s >= z & z in (D1 "\/" D2) by A1;



       A4: ( uparrow (( uparrow D1) "\/" ( uparrow D2))) = { x where x be Element of L : ex t be Element of L st x >= t & t in (( uparrow D1) "\/" ( uparrow D2)) } by WAYBEL_0: 15;



       A5: D1 is Subset of ( uparrow D1) & D2 is Subset of ( uparrow D2) by WAYBEL_0: 16;

      consider x be Element of L such that

       A6: s >= x and

       A7: x in (D1 "\/" D2) by A3;

      ex a,b be Element of L st x = (a "\/" b) & a in D1 & b in D2 by A7;

      then x in (( uparrow D1) "\/" ( uparrow D2)) by A5;

      hence thesis by A4, A2, A6;

    end;

    begin

    definition

      let L be non empty RelStr, D1,D2 be Subset of L;

      :: YELLOW_4:def4

      func D1 "/\" D2 -> Subset of L equals { (x "/\" y) where x,y be Element of L : x in D1 & y in D2 };

      coherence

      proof

        { (x "/\" y) where x,y be Element of L : x in D1 & y in D2 } c= the carrier of L

        proof

          let q be object;

          assume q in { (x "/\" y) where x,y be Element of L : x in D1 & y in D2 };

          then ex a,b be Element of L st q = (a "/\" b) & a in D1 & b in D2;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let L be with_infima antisymmetric RelStr, D1,D2 be Subset of L;

      :: original: "/\"

      redefine

      func D1 "/\" D2;

      commutativity

      proof

        let D1,D2 be Subset of L;

        thus (D1 "/\" D2) c= (D2 "/\" D1)

        proof

          let q be object;

          assume q in (D1 "/\" D2);

          then ex x,y be Element of L st q = (x "/\" y) & x in D1 & y in D2;

          hence thesis;

        end;

        let q be object;

        assume q in (D2 "/\" D1);

        then ex x,y be Element of L st q = (x "/\" y) & x in D2 & y in D1;

        hence thesis;

      end;

    end

    theorem :: YELLOW_4:36

    for L be non empty RelStr, X be Subset of L holds (X "/\" ( {} L)) = {}

    proof

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

      thus (X "/\" ( {} L)) c= {}

      proof

        let a be object;

        assume a in (X "/\" ( {} L));

        then ex s,t be Element of L st a = (s "/\" t) & s in X & t in ( {} L);

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: YELLOW_4:37

    for L be non empty RelStr, X,Y be Subset of L, x,y be Element of L st x in X & y in Y holds (x "/\" y) in (X "/\" Y);

    theorem :: YELLOW_4:38

    for L be antisymmetric with_infima RelStr holds for A be Subset of L, B be non empty Subset of L holds A is_coarser_than (A "/\" B)

    proof

      let L be antisymmetric with_infima RelStr, A be Subset of L, B be non empty Subset of L;

      consider b be object such that

       A1: b in B by XBOOLE_0:def 1;

      reconsider b as Element of B by A1;

      let q be Element of L such that

       A2: q in A;

      take (q "/\" b);

      thus (q "/\" b) in (A "/\" B) by A2;

      thus thesis by YELLOW_0: 23;

    end;

    theorem :: YELLOW_4:39

    for L be antisymmetric with_infima RelStr holds for A,B be Subset of L holds (A "/\" B) is_finer_than A

    proof

      let L be antisymmetric with_infima RelStr, A,B be Subset of L;

      let q be Element of L;

      assume q in (A "/\" B);

      then

      consider x,y be Element of L such that

       A1: q = (x "/\" y) and

       A2: x in A and y in B;

      take x;

      thus x in A by A2;

      thus thesis by A1, YELLOW_0: 23;

    end;

    theorem :: YELLOW_4:40

    for L be antisymmetric reflexive with_infima RelStr holds for A be Subset of L holds A c= (A "/\" A)

    proof

      let L be antisymmetric reflexive with_infima RelStr, A be Subset of L;

      let q be object;

      assume

       A1: q in A;

      then

      reconsider A1 = A as non empty Subset of L;

      reconsider q1 = q as Element of A1 by A1;

      q1 = (q1 "/\" q1) by YELLOW_0: 25;

      hence thesis;

    end;

    theorem :: YELLOW_4:41

    for L be with_infima antisymmetric transitive RelStr holds for D1,D2,D3 be Subset of L holds ((D1 "/\" D2) "/\" D3) = (D1 "/\" (D2 "/\" D3))

    proof

      let L be with_infima antisymmetric transitive RelStr, D1,D2,D3 be Subset of L;

      thus ((D1 "/\" D2) "/\" D3) c= (D1 "/\" (D2 "/\" D3))

      proof

        let q be object;

        assume q in ((D1 "/\" D2) "/\" D3);

        then

        consider a1,b1 be Element of L such that

         A1: q = (a1 "/\" b1) and

         A2: a1 in (D1 "/\" D2) and

         A3: b1 in D3;

        consider a11,b11 be Element of L such that

         A4: a1 = (a11 "/\" b11) and

         A5: a11 in D1 and

         A6: b11 in D2 by A2;

        (b11 "/\" b1) in (D2 "/\" D3) & q = (a11 "/\" (b11 "/\" b1)) by A1, A3, A4, A6, LATTICE3: 16;

        hence thesis by A5;

      end;

      let q be object;

      assume q in (D1 "/\" (D2 "/\" D3));

      then

      consider a1,b1 be Element of L such that

       A7: q = (a1 "/\" b1) & a1 in D1 and

       A8: b1 in (D2 "/\" D3);

      consider a11,b11 be Element of L such that

       A9: b1 = (a11 "/\" b11) & a11 in D2 and

       A10: b11 in D3 by A8;

      (a1 "/\" a11) in (D1 "/\" D2) & q = ((a1 "/\" a11) "/\" b11) by A7, A9, LATTICE3: 16;

      hence thesis by A10;

    end;

    registration

      let L be non empty RelStr, D1,D2 be non empty Subset of L;

      cluster (D1 "/\" D2) -> non empty;

      coherence

      proof

        consider b be object such that

         A1: b in D2 by XBOOLE_0:def 1;

        reconsider b as Element of D2 by A1;

        consider a be object such that

         A2: a in D1 by XBOOLE_0:def 1;

        reconsider a as Element of D1 by A2;

        (a "/\" b) in { (x "/\" y) where x,y be Element of L : x in D1 & y in D2 };

        hence thesis;

      end;

    end

    registration

      let L be with_infima transitive antisymmetric RelStr, D1,D2 be directed Subset of L;

      cluster (D1 "/\" D2) -> directed;

      coherence

      proof

        let a,b be Element of L;

        set X = (D1 "/\" D2);

        assume that

         A1: a in X and

         A2: b in X;

        consider x,y be Element of L such that

         A3: a = (x "/\" y) and

         A4: x in D1 and

         A5: y in D2 by A1;

        consider s,t be Element of L such that

         A6: b = (s "/\" t) and

         A7: s in D1 and

         A8: t in D2 by A2;

        consider z2 be Element of L such that

         A9: z2 in D2 and

         A10: y <= z2 & t <= z2 by A5, A8, WAYBEL_0:def 1;

        consider z1 be Element of L such that

         A11: z1 in D1 and

         A12: x <= z1 & s <= z1 by A4, A7, WAYBEL_0:def 1;

        take z = (z1 "/\" z2);

        thus z in X by A11, A9;

        thus thesis by A3, A6, A12, A10, YELLOW_3: 2;

      end;

    end

    registration

      let L be with_infima transitive antisymmetric RelStr, D1,D2 be filtered Subset of L;

      cluster (D1 "/\" D2) -> filtered;

      coherence

      proof

        let a,b be Element of L;

        set X = (D1 "/\" D2);

        assume that

         A1: a in X and

         A2: b in X;

        consider x,y be Element of L such that

         A3: a = (x "/\" y) and

         A4: x in D1 and

         A5: y in D2 by A1;

        consider s,t be Element of L such that

         A6: b = (s "/\" t) and

         A7: s in D1 and

         A8: t in D2 by A2;

        consider z2 be Element of L such that

         A9: z2 in D2 and

         A10: y >= z2 & t >= z2 by A5, A8, WAYBEL_0:def 2;

        consider z1 be Element of L such that

         A11: z1 in D1 and

         A12: x >= z1 & s >= z1 by A4, A7, WAYBEL_0:def 2;

        take z = (z1 "/\" z2);

        thus z in X by A11, A9;

        thus thesis by A3, A6, A12, A10, YELLOW_3: 2;

      end;

    end

    registration

      let L be Semilattice, D1,D2 be lower Subset of L;

      cluster (D1 "/\" D2) -> lower;

      coherence

      proof

        set X = (D1 "/\" D2);

        let a,b be Element of L such that

         A1: a in X and

         A2: b <= a;

        consider x,y be Element of L such that

         A3: a = (x "/\" y) and

         A4: x in D1 and

         A5: y in D2 by A1;



         A6: ex xx be Element of L st x >= xx & y >= xx & for c be Element of L st x >= c & y >= c holds xx >= c by LATTICE3:def 11;

        then (x "/\" y) <= x by LATTICE3:def 14;

        then b <= x by A2, A3, YELLOW_0:def 2;

        then

         A7: b in D1 by A4, WAYBEL_0:def 19;

        (x "/\" y) <= y by A6, LATTICE3:def 14;

        then b <= y by A2, A3, YELLOW_0:def 2;

        then

         A8: b in D2 by A5, WAYBEL_0:def 19;

        b = (b "/\" b) by YELLOW_0: 25;

        hence thesis by A7, A8;

      end;

    end

    theorem :: YELLOW_4:42



     Th42: for L be non empty RelStr, Y be Subset of L, x be Element of L holds ( {x} "/\" Y) = { (x "/\" y) where y be Element of L : y in Y }

    proof

      let L be non empty RelStr, Y be Subset of L, x be Element of L;

      thus ( {x} "/\" Y) c= { (x "/\" y) where y be Element of L : y in Y }

      proof

        let q be object;

        assume q in ( {x} "/\" Y);

        then

        consider s,t be Element of L such that

         A1: q = (s "/\" t) and

         A2: s in {x} and

         A3: t in Y;

        s = x by A2, TARSKI:def 1;

        hence thesis by A1, A3;

      end;

      let q be object;

      assume q in { (x "/\" y) where y be Element of L : y in Y };

      then

       A4: ex y be Element of L st q = (x "/\" y) & y in Y;

      x in {x} by TARSKI:def 1;

      hence thesis by A4;

    end;

    theorem :: YELLOW_4:43

    for L be non empty RelStr, A,B,C be Subset of L holds (A "/\" (B \/ C)) = ((A "/\" B) \/ (A "/\" C))

    proof

      let L be non empty RelStr, A,B,C be Subset of L;

      thus (A "/\" (B \/ C)) c= ((A "/\" B) \/ (A "/\" C))

      proof

        let q be object;

        assume q in (A "/\" (B \/ C));

        then

        consider a,y be Element of L such that

         A1: q = (a "/\" y) & a in A and

         A2: y in (B \/ C);

        y in B or y in C by A2, XBOOLE_0:def 3;

        then q in (A "/\" B) or q in (A "/\" C) by A1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let q be object such that

       A3: q in ((A "/\" B) \/ (A "/\" C));

      per cases by A3, XBOOLE_0:def 3;

        suppose q in (A "/\" B);

        then

        consider a,b be Element of L such that

         A4: q = (a "/\" b) & a in A and

         A5: b in B;

        b in (B \/ C) by A5, XBOOLE_0:def 3;

        hence thesis by A4;

      end;

        suppose q in (A "/\" C);

        then

        consider a,b be Element of L such that

         A6: q = (a "/\" b) & a in A and

         A7: b in C;

        b in (B \/ C) by A7, XBOOLE_0:def 3;

        hence thesis by A6;

      end;

    end;

    theorem :: YELLOW_4:44

    for L be antisymmetric reflexive with_infima RelStr holds for A,B,C be Subset of L holds (A \/ (B "/\" C)) c= ((A \/ B) "/\" (A \/ C))

    proof

      let L be antisymmetric reflexive with_infima RelStr, A,B,C be Subset of L;

      let q be object such that

       A1: q in (A \/ (B "/\" C));

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: q in A;

        then

        reconsider q1 = q as Element of L;



         A3: q1 = (q1 "/\" q1) by YELLOW_0: 25;

        q1 in (A \/ B) & q1 in (A \/ C) by A2, XBOOLE_0:def 3;

        hence thesis by A3;

      end;

        suppose q in (B "/\" C);

        then

        consider b,c be Element of L such that

         A4: q = (b "/\" c) and

         A5: b in B & c in C;

        b in (A \/ B) & c in (A \/ C) by A5, XBOOLE_0:def 3;

        hence thesis by A4;

      end;

    end;

    theorem :: YELLOW_4:45

    for L be antisymmetric with_infima RelStr, A be lower Subset of L holds for B,C be Subset of L holds ((A \/ B) "/\" (A \/ C)) c= (A \/ (B "/\" C))

    proof

      let L be antisymmetric with_infima RelStr, A be lower Subset of L, B,C be Subset of L;

      let q be object;

      assume q in ((A \/ B) "/\" (A \/ C));

      then

      consider x,y be Element of L such that

       A1: q = (x "/\" y) and

       A2: x in (A \/ B) & y in (A \/ C);



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



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

      per cases by A2, XBOOLE_0:def 3;

        suppose x in A & y in A;

        then q in A by A1, A3, WAYBEL_0:def 19;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose x in A & y in C;

        then q in A by A1, A3, WAYBEL_0:def 19;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose x in B & y in A;

        then q in A by A1, A4, WAYBEL_0:def 19;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose x in B & y in C;

        then (x "/\" y) in (B "/\" C);

        hence thesis by A1, XBOOLE_0:def 3;

      end;

    end;

     Lm3:

    now

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

      thus { (a "/\" b) where a,b be Element of L : a in {x} & b in {y} } = {(x "/\" y)}

      proof

        thus { (a "/\" b) where a,b be Element of L : a in {x} & b in {y} } c= {(x "/\" y)}

        proof

          let q be object;

          assume q in { (a "/\" b) where a,b be Element of L : a in {x} & b in {y} };

          then

          consider u,v be Element of L such that

           A1: q = (u "/\" v) and

           A2: u in {x} & v in {y};

          u = x & v = y by A2, TARSKI:def 1;

          hence thesis by A1, TARSKI:def 1;

        end;

        let q be object;

        assume q in {(x "/\" y)};

        then

         A3: q = (x "/\" y) by TARSKI:def 1;

        x in {x} & y in {y} by TARSKI:def 1;

        hence thesis by A3;

      end;

    end;

     Lm4:

    now

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

      thus { (a "/\" b) where a,b be Element of L : a in {x} & b in {y, z} } = {(x "/\" y), (x "/\" z)}

      proof

        thus { (a "/\" b) where a,b be Element of L : a in {x} & b in {y, z} } c= {(x "/\" y), (x "/\" z)}

        proof

          let q be object;

          assume q in { (a "/\" b) where a,b be Element of L : a in {x} & b in {y, z} };

          then

          consider u,v be Element of L such that

           A1: q = (u "/\" v) and

           A2: u in {x} and

           A3: v in {y, z};



           A4: v = y or v = z by A3, TARSKI:def 2;

          u = x by A2, TARSKI:def 1;

          hence thesis by A1, A4, TARSKI:def 2;

        end;

        let q be object;



         A5: z in {y, z} by TARSKI:def 2;

        assume q in {(x "/\" y), (x "/\" z)};

        then

         A6: q = (x "/\" y) or q = (x "/\" z) by TARSKI:def 2;

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

        hence thesis by A6, A5;

      end;

    end;

    theorem :: YELLOW_4:46

    for L be non empty RelStr, x,y be Element of L holds ( {x} "/\" {y}) = {(x "/\" y)} by Lm3;

    theorem :: YELLOW_4:47

    for L be non empty RelStr, x,y,z be Element of L holds ( {x} "/\" {y, z}) = {(x "/\" y), (x "/\" z)} by Lm4;

    theorem :: YELLOW_4:48

    for L be non empty RelStr, X1,X2,Y1,Y2 be Subset of L st X1 c= Y1 & X2 c= Y2 holds (X1 "/\" X2) c= (Y1 "/\" Y2)

    proof

      let L be non empty RelStr, X1,X2,Y1,Y2 be Subset of L such that

       A1: X1 c= Y1 & X2 c= Y2;

      let q be object;

      assume q in (X1 "/\" X2);

      then ex x,y be Element of L st q = (x "/\" y) & x in X1 & y in X2;

      hence thesis by A1;

    end;

    theorem :: YELLOW_4:49



     Th49: for L be antisymmetric reflexive with_infima RelStr holds for A,B be Subset of L holds (A /\ B) c= (A "/\" B)

    proof

      let L be antisymmetric reflexive with_infima RelStr, A,B be Subset of L;

      let q be object;

      assume

       A1: q in (A /\ B);

      then

      reconsider A1 = A as non empty Subset of L;

      reconsider q1 = q as Element of A1 by A1, XBOOLE_0:def 4;



       A2: q1 = (q1 "/\" q1) by YELLOW_0: 25;

      q in B by A1, XBOOLE_0:def 4;

      hence thesis by A2;

    end;

    theorem :: YELLOW_4:50



     Th50: for L be antisymmetric reflexive with_infima RelStr holds for A,B be lower Subset of L holds (A "/\" B) = (A /\ B)

    proof

      let L be antisymmetric reflexive with_infima RelStr, A,B be lower Subset of L;

      thus (A "/\" B) c= (A /\ B)

      proof

        let q be object;

        assume q in (A "/\" B);

        then

        consider x,y be Element of L such that

         A1: q = (x "/\" y) and

         A2: x in A and

         A3: y in B;



         A4: ex z be Element of L st x >= z & y >= z & for c be Element of L st x >= c & y >= c holds z >= c by LATTICE3:def 11;

        then (x "/\" y) <= y by LATTICE3:def 14;

        then

         A5: q in B by A1, A3, WAYBEL_0:def 19;

        (x "/\" y) <= x by A4, LATTICE3:def 14;

        then q in A by A1, A2, WAYBEL_0:def 19;

        hence thesis by A5, XBOOLE_0:def 4;

      end;

      thus thesis by Th49;

    end;

    theorem :: YELLOW_4:51

    for L be with_infima reflexive antisymmetric RelStr holds for D be Subset of L, x be Element of L st x is_>=_than D holds ( {x} "/\" D) = D

    proof

      let L be with_infima reflexive antisymmetric RelStr, D be Subset of L, x be Element of L such that

       A1: x is_>=_than D;



       A2: ( {x} "/\" D) = { (x "/\" y) where y be Element of L : y in D } by Th42;

      thus ( {x} "/\" D) c= D

      proof

        let q be object;

        assume q in ( {x} "/\" D);

        then

        consider y be Element of L such that

         A3: q = (x "/\" y) and

         A4: y in D by A2;

        x >= y by A1, A4;

        hence thesis by A3, A4, YELLOW_0: 25;

      end;

      let q be object;

      assume

       A5: q in D;

      then

      reconsider D1 = D as non empty Subset of L;

      reconsider y = q as Element of D1 by A5;

      x >= y by A1;

      then q = (x "/\" y) by YELLOW_0: 25;

      hence thesis by A2;

    end;

    theorem :: YELLOW_4:52

    for L be with_infima antisymmetric RelStr holds for D be Subset of L, x be Element of L holds ( {x} "/\" D) is_<=_than x

    proof

      let L be with_infima antisymmetric RelStr, D be Subset of L, x be Element of L;

      let b be Element of L;



       A1: ( {x} "/\" D) = { (x "/\" h) where h be Element of L : h in D } by Th42;

      assume b in ( {x} "/\" D);

      then

      consider h be Element of L such that

       A2: b = (x "/\" h) and h in D by A1;

      ex w be Element of L st x >= w & h >= w & for c be Element of L st x >= c & h >= c holds w >= c by LATTICE3:def 11;

      hence thesis by A2, LATTICE3:def 14;

    end;

    theorem :: YELLOW_4:53

    for L be Semilattice, X be Subset of L, x be Element of L st ex_sup_of (( {x} "/\" X),L) & ex_sup_of (X,L) holds ( sup ( {x} "/\" X)) <= (x "/\" ( sup X))

    proof

      let L be Semilattice, X be Subset of L, x be Element of L such that

       A1: ex_sup_of (( {x} "/\" X),L) and

       A2: ex_sup_of (X,L);



       A3: ( {x} "/\" X) = { (x "/\" y) where y be Element of L : y in X } by Th42;

      ( {x} "/\" X) is_<=_than (x "/\" ( sup X))

      proof

        let q be Element of L;

        assume q in ( {x} "/\" X);

        then

        consider y be Element of L such that

         A4: q = (x "/\" y) and

         A5: y in X by A3;

        x <= x & y <= ( sup X) by A2, A5, Th1;

        hence q <= (x "/\" ( sup X)) by A4, YELLOW_3: 2;

      end;

      hence thesis by A1, YELLOW_0:def 9;

    end;

    theorem :: YELLOW_4:54



     Th54: for L be complete transitive antisymmetric non empty RelStr holds for A be Subset of L, B be non empty Subset of L holds A is_>=_than ( inf (A "/\" B))

    proof

      let L be complete transitive antisymmetric non empty RelStr, A be Subset of L, B be non empty Subset of L;

      set b = the Element of B;

      let x be Element of L;

      assume x in A;

      then

       A1: (x "/\" b) in (A "/\" B);

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

      then

       A2: x >= (x "/\" b) by LATTICE3:def 14;

       ex_inf_of ((A "/\" B),L) by YELLOW_0: 17;

      then (A "/\" B) is_>=_than ( inf (A "/\" B)) by YELLOW_0:def 10;

      then (x "/\" b) >= ( inf (A "/\" B)) by A1;

      hence thesis by A2, YELLOW_0:def 2;

    end;

    theorem :: YELLOW_4:55



     Th55: for L be with_infima transitive antisymmetric RelStr holds for a,b be Element of L, A,B be Subset of L st a is_<=_than A & b is_<=_than B holds (a "/\" b) is_<=_than (A "/\" B)

    proof

      let L be with_infima transitive antisymmetric RelStr, a,b be Element of L, A,B be Subset of L such that

       A1: a is_<=_than A & b is_<=_than B;

      let q be Element of L;

      assume q in (A "/\" B);

      then

      consider x,y be Element of L such that

       A2: q = (x "/\" y) and

       A3: x in A & y in B;

      a <= x & b <= y by A1, A3;

      hence thesis by A2, YELLOW_3: 2;

    end;

    theorem :: YELLOW_4:56

    for L be with_infima transitive antisymmetric RelStr holds for a,b be Element of L, A,B be Subset of L st a is_>=_than A & b is_>=_than B holds (a "/\" b) is_>=_than (A "/\" B)

    proof

      let L be with_infima transitive antisymmetric RelStr, a,b be Element of L, A,B be Subset of L such that

       A1: a is_>=_than A & b is_>=_than B;

      let q be Element of L;

      assume q in (A "/\" B);

      then

      consider x,y be Element of L such that

       A2: q = (x "/\" y) and

       A3: x in A & y in B;

      a >= x & b >= y by A1, A3;

      hence thesis by A2, YELLOW_3: 2;

    end;

    theorem :: YELLOW_4:57

    for L be complete non empty Poset holds for A,B be non empty Subset of L holds ( inf (A "/\" B)) = (( inf A) "/\" ( inf B))

    proof

      let L be complete non empty Poset, A,B be non empty Subset of L;

      B is_>=_than ( inf (A "/\" B)) by Th54;

      then

       A1: ( inf B) >= ( inf (A "/\" B)) by YELLOW_0: 33;

      A is_>=_than ( inf (A "/\" B)) by Th54;

      then ( inf A) >= ( inf (A "/\" B)) by YELLOW_0: 33;

      then

       A2: (( inf A) "/\" ( inf B)) >= (( inf (A "/\" B)) "/\" ( inf (A "/\" B))) by A1, YELLOW_3: 2;

      A is_>=_than ( inf A) & B is_>=_than ( inf B) by YELLOW_0: 33;

      then ex_inf_of ((A "/\" B),L) & (A "/\" B) is_>=_than (( inf A) "/\" ( inf B)) by Th55, YELLOW_0: 17;

      then

       A3: ( inf (A "/\" B)) >= (( inf A) "/\" ( inf B)) by YELLOW_0:def 10;

      (( inf (A "/\" B)) "/\" ( inf (A "/\" B))) = ( inf (A "/\" B)) by YELLOW_0: 25;

      hence thesis by A3, A2, ORDERS_2: 2;

    end;

    theorem :: YELLOW_4:58

    for L be Semilattice, x,y be Element of ( InclPoset ( Ids L)) holds for x1,y1 be Subset of L st x = x1 & y = y1 holds (x "/\" y) = (x1 "/\" y1)

    proof

      let L be Semilattice, x,y be Element of ( InclPoset ( Ids L)), x1,y1 be Subset of L;

      assume

       A1: x = x1 & y = y1;

      then

       A2: x1 is lower & y1 is lower by YELLOW_2: 41;



      thus (x "/\" y) = (x /\ y) by YELLOW_2: 43

      .= (x1 "/\" y1) by A1, A2, Th50;

    end;

    theorem :: YELLOW_4:59

    for L be with_infima antisymmetric RelStr holds for X be Subset of L, Y be non empty Subset of L holds X c= ( uparrow (X "/\" Y))

    proof

      let L be with_infima antisymmetric RelStr, X be Subset of L, Y be non empty Subset of L;

      consider y be object such that

       A1: y in Y by XBOOLE_0:def 1;

      reconsider y as Element of Y by A1;

      let q be object;

      assume

       A2: q in X;

      then

      reconsider X1 = X as non empty Subset of L;

      reconsider x = q as Element of X1 by A2;

      ex s be Element of L st x >= s & y >= s & for c be Element of L st x >= c & y >= c holds s >= c by LATTICE3:def 11;

      then

       A3: (x "/\" y) <= x by LATTICE3:def 14;

      ( uparrow (X "/\" Y)) = { s where s be Element of L : ex y be Element of L st s >= y & y in (X "/\" Y) } & (x "/\" y) in (X1 "/\" Y) by WAYBEL_0: 15;

      hence thesis by A3;

    end;

    theorem :: YELLOW_4:60

    for L be non empty RelStr, D be Subset of [:L, L:] holds ( union { X where X be Subset of L : ex x be Element of L st X = ( {x} "/\" ( proj2 D)) & x in ( proj1 D) }) = (( proj1 D) "/\" ( proj2 D))

    proof

      let L be non empty RelStr, D be Subset of [:L, L:];

      set D1 = ( proj1 D), D2 = ( proj2 D);

      defpred P[ set] means ex x be Element of L st $1 = ( {x} "/\" ( proj2 D)) & x in ( proj1 D);

      thus ( union { X where X be Subset of L : P[X] }) c= (D1 "/\" D2)

      proof

        let q be object;

        assume q in ( union { X where X be Subset of L : P[X] });

        then

        consider w be set such that

         A1: q in w and

         A2: w in { X where X be Subset of L : P[X] } by TARSKI:def 4;

        consider e be Subset of L such that

         A3: w = e and

         A4: P[e] by A2;

        consider p be Element of L such that

         A5: e = ( {p} "/\" D2) and

         A6: p in D1 by A4;

        ( {p} "/\" D2) = { (p "/\" y) where y be Element of L : y in D2 } by Th42;

        then ex y be Element of L st q = (p "/\" y) & y in D2 by A1, A3, A5;

        hence thesis by A6;

      end;

      let q be object;

      assume q in (D1 "/\" D2);

      then

      consider x,y be Element of L such that

       A7: q = (x "/\" y) and

       A8: x in D1 and

       A9: y in D2;

      ( {x} "/\" D2) = { (x "/\" d) where d be Element of L : d in D2 } by Th42;

      then

       A10: q in ( {x} "/\" D2) by A7, A9;

      ( {x} "/\" D2) in { X where X be Subset of L : P[X] } by A8;

      hence thesis by A10, TARSKI:def 4;

    end;

    theorem :: YELLOW_4:61



     Th61: for L be transitive antisymmetric with_infima RelStr holds for D1,D2 be Subset of L holds ( downarrow (( downarrow D1) "/\" ( downarrow D2))) c= ( downarrow (D1 "/\" D2))

    proof

      let L be transitive antisymmetric with_infima RelStr, D1,D2 be Subset of L;



       A1: ( downarrow (( downarrow D1) "/\" ( downarrow D2))) = { x where x be Element of L : ex t be Element of L st x <= t & t in (( downarrow D1) "/\" ( downarrow D2)) } by WAYBEL_0: 14;

      let y be object;

      assume y in ( downarrow (( downarrow D1) "/\" ( downarrow D2)));

      then

      consider x be Element of L such that

       A2: y = x and

       A3: ex t be Element of L st x <= t & t in (( downarrow D1) "/\" ( downarrow D2)) by A1;

      consider x1 be Element of L such that

       A4: x <= x1 and

       A5: x1 in (( downarrow D1) "/\" ( downarrow D2)) by A3;

      consider a,b be Element of L such that

       A6: x1 = (a "/\" b) and

       A7: a in ( downarrow D1) and

       A8: b in ( downarrow D2) by A5;

      ( downarrow D2) = { s2 where s2 be Element of L : ex z be Element of L st s2 <= z & z in D2 } by WAYBEL_0: 14;

      then

      consider B1 be Element of L such that

       A9: b = B1 and

       A10: ex z be Element of L st B1 <= z & z in D2 by A8;

      consider b1 be Element of L such that

       A11: B1 <= b1 and

       A12: b1 in D2 by A10;

      ( downarrow D1) = { s1 where s1 be Element of L : ex z be Element of L st s1 <= z & z in D1 } by WAYBEL_0: 14;

      then

      consider A1 be Element of L such that

       A13: a = A1 and

       A14: ex z be Element of L st A1 <= z & z in D1 by A7;

      consider a1 be Element of L such that

       A15: A1 <= a1 and

       A16: a1 in D1 by A14;

      x1 <= (a1 "/\" b1) by A6, A13, A9, A15, A11, YELLOW_3: 2;

      then

       A17: ( downarrow (D1 "/\" D2)) = { s where s be Element of L : ex z be Element of L st s <= z & z in (D1 "/\" D2) } & x <= (a1 "/\" b1) by A4, ORDERS_2: 3, WAYBEL_0: 14;

      (a1 "/\" b1) in (D1 "/\" D2) by A16, A12;

      hence thesis by A2, A17;

    end;

    theorem :: YELLOW_4:62

    for L be Semilattice, D1,D2 be Subset of L holds ( downarrow (( downarrow D1) "/\" ( downarrow D2))) = ( downarrow (D1 "/\" D2))

    proof

      let L be Semilattice, D1,D2 be Subset of L;



       A1: ( downarrow (D1 "/\" D2)) = { s where s be Element of L : ex z be Element of L st s <= z & z in (D1 "/\" D2) } by WAYBEL_0: 14;

      thus ( downarrow (( downarrow D1) "/\" ( downarrow D2))) c= ( downarrow (D1 "/\" D2)) by Th61;

      let q be object;

      assume q in ( downarrow (D1 "/\" D2));

      then

      consider s be Element of L such that

       A2: q = s and

       A3: ex z be Element of L st s <= z & z in (D1 "/\" D2) by A1;



       A4: ( downarrow (( downarrow D1) "/\" ( downarrow D2))) = { x where x be Element of L : ex t be Element of L st x <= t & t in (( downarrow D1) "/\" ( downarrow D2)) } by WAYBEL_0: 14;



       A5: D1 is Subset of ( downarrow D1) & D2 is Subset of ( downarrow D2) by WAYBEL_0: 16;

      consider x be Element of L such that

       A6: s <= x and

       A7: x in (D1 "/\" D2) by A3;

      ex a,b be Element of L st x = (a "/\" b) & a in D1 & b in D2 by A7;

      then x in (( downarrow D1) "/\" ( downarrow D2)) by A5;

      hence thesis by A4, A2, A6;

    end;

    theorem :: YELLOW_4:63



     Th63: for L be transitive antisymmetric with_infima RelStr holds for D1,D2 be Subset of L holds ( uparrow (( uparrow D1) "/\" ( uparrow D2))) c= ( uparrow (D1 "/\" D2))

    proof

      let L be transitive antisymmetric with_infima RelStr, D1,D2 be Subset of L;



       A1: ( uparrow (( uparrow D1) "/\" ( uparrow D2))) = { x where x be Element of L : ex t be Element of L st x >= t & t in (( uparrow D1) "/\" ( uparrow D2)) } by WAYBEL_0: 15;

      let y be object;

      assume y in ( uparrow (( uparrow D1) "/\" ( uparrow D2)));

      then

      consider x be Element of L such that

       A2: y = x and

       A3: ex t be Element of L st x >= t & t in (( uparrow D1) "/\" ( uparrow D2)) by A1;

      consider x1 be Element of L such that

       A4: x >= x1 and

       A5: x1 in (( uparrow D1) "/\" ( uparrow D2)) by A3;

      consider a,b be Element of L such that

       A6: x1 = (a "/\" b) and

       A7: a in ( uparrow D1) and

       A8: b in ( uparrow D2) by A5;

      ( uparrow D2) = { s2 where s2 be Element of L : ex z be Element of L st s2 >= z & z in D2 } by WAYBEL_0: 15;

      then

      consider B1 be Element of L such that

       A9: b = B1 and

       A10: ex z be Element of L st B1 >= z & z in D2 by A8;

      consider b1 be Element of L such that

       A11: B1 >= b1 and

       A12: b1 in D2 by A10;

      ( uparrow D1) = { s1 where s1 be Element of L : ex z be Element of L st s1 >= z & z in D1 } by WAYBEL_0: 15;

      then

      consider A1 be Element of L such that

       A13: a = A1 and

       A14: ex z be Element of L st A1 >= z & z in D1 by A7;

      consider a1 be Element of L such that

       A15: A1 >= a1 and

       A16: a1 in D1 by A14;

      x1 >= (a1 "/\" b1) by A6, A13, A9, A15, A11, YELLOW_3: 2;

      then

       A17: ( uparrow (D1 "/\" D2)) = { s where s be Element of L : ex z be Element of L st s >= z & z in (D1 "/\" D2) } & x >= (a1 "/\" b1) by A4, ORDERS_2: 3, WAYBEL_0: 15;

      (a1 "/\" b1) in (D1 "/\" D2) by A16, A12;

      hence thesis by A2, A17;

    end;

    theorem :: YELLOW_4:64

    for L be Semilattice, D1,D2 be Subset of L holds ( uparrow (( uparrow D1) "/\" ( uparrow D2))) = ( uparrow (D1 "/\" D2))

    proof

      let L be Semilattice, D1,D2 be Subset of L;



       A1: ( uparrow (D1 "/\" D2)) = { s where s be Element of L : ex z be Element of L st s >= z & z in (D1 "/\" D2) } by WAYBEL_0: 15;

      thus ( uparrow (( uparrow D1) "/\" ( uparrow D2))) c= ( uparrow (D1 "/\" D2)) by Th63;

      let q be object;

      assume q in ( uparrow (D1 "/\" D2));

      then

      consider s be Element of L such that

       A2: q = s and

       A3: ex z be Element of L st s >= z & z in (D1 "/\" D2) by A1;



       A4: ( uparrow (( uparrow D1) "/\" ( uparrow D2))) = { x where x be Element of L : ex t be Element of L st x >= t & t in (( uparrow D1) "/\" ( uparrow D2)) } by WAYBEL_0: 15;



       A5: D1 is Subset of ( uparrow D1) & D2 is Subset of ( uparrow D2) by WAYBEL_0: 16;

      consider x be Element of L such that

       A6: s >= x and

       A7: x in (D1 "/\" D2) by A3;

      ex a,b be Element of L st x = (a "/\" b) & a in D1 & b in D2 by A7;

      then x in (( uparrow D1) "/\" ( uparrow D2)) by A5;

      hence thesis by A4, A2, A6;

    end;