yellow10.miz



    begin

    registration

      let S,T be non empty upper-bounded RelStr;

      cluster [:S, T:] -> upper-bounded;

      coherence

      proof

        

         A1: the carrier of T c= the carrier of T;

        consider t be Element of T such that

         A2: t is_>=_than the carrier of T by YELLOW_0:def 5;

        consider s be Element of S such that

         A3: s is_>=_than the carrier of S by YELLOW_0:def 5;

        take [s, t];

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] & the carrier of S c= the carrier of S by YELLOW_3:def 2;

        hence thesis by A3, A2, A1, YELLOW_3: 30;

      end;

    end

    registration

      let S,T be non empty lower-bounded RelStr;

      cluster [:S, T:] -> lower-bounded;

      coherence

      proof

        

         A1: the carrier of T c= the carrier of T;

        consider t be Element of T such that

         A2: t is_<=_than the carrier of T by YELLOW_0:def 4;

        consider s be Element of S such that

         A3: s is_<=_than the carrier of S by YELLOW_0:def 4;

        take [s, t];

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] & the carrier of S c= the carrier of S by YELLOW_3:def 2;

        hence thesis by A3, A2, A1, YELLOW_3: 33;

      end;

    end

    theorem :: YELLOW10:1

    for S,T be non empty RelStr st [:S, T:] is upper-bounded holds S is upper-bounded & T is upper-bounded

    proof

      let S,T be non empty RelStr;

      given x be Element of [:S, T:] such that

       A1: x is_>=_than the carrier of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      consider s,t be object such that

       A2: s in the carrier of S and

       A3: t in the carrier of T and

       A4: x = [s, t] by ZFMISC_1:def 2;

      reconsider t as Element of T by A3;

      reconsider s as Element of S by A2;

      

       A5: the carrier of S c= the carrier of S & the carrier of T c= the carrier of T;

      

       A6: [s, t] is_>=_than [:the carrier of S, the carrier of T:] by A1, A4;

      thus S is upper-bounded

      proof

        take s;

        thus thesis by A5, A6, YELLOW_3: 29;

      end;

      take t;

      thus thesis by A5, A6, YELLOW_3: 29;

    end;

    theorem :: YELLOW10:2

    for S,T be non empty RelStr st [:S, T:] is lower-bounded holds S is lower-bounded & T is lower-bounded

    proof

      let S,T be non empty RelStr;

      given x be Element of [:S, T:] such that

       A1: x is_<=_than the carrier of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      consider s,t be object such that

       A2: s in the carrier of S and

       A3: t in the carrier of T and

       A4: x = [s, t] by ZFMISC_1:def 2;

      reconsider t as Element of T by A3;

      reconsider s as Element of S by A2;

      

       A5: the carrier of S c= the carrier of S & the carrier of T c= the carrier of T;

      

       A6: [s, t] is_<=_than [:the carrier of S, the carrier of T:] by A1, A4;

      thus S is lower-bounded

      proof

        take s;

        thus thesis by A5, A6, YELLOW_3: 32;

      end;

      take t;

      thus thesis by A5, A6, YELLOW_3: 32;

    end;

    theorem :: YELLOW10:3

    

     Th3: for S,T be upper-bounded antisymmetric non empty RelStr holds ( Top [:S, T:]) = [( Top S), ( Top T)]

    proof

      let S,T be upper-bounded antisymmetric non empty RelStr;

      

       A1: for a be Element of [:S, T:] st {} is_>=_than a holds a <= [( Top S), ( Top T)]

      proof

        let a be Element of [:S, T:];

        assume {} is_>=_than a;

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

        consider s,t be object such that

         A2: s in the carrier of S and

         A3: t in the carrier of T and

         A4: a = [s, t] by ZFMISC_1:def 2;

        reconsider t as Element of T by A3;

        reconsider s as Element of S by A2;

        s <= ( Top S) & t <= ( Top T) by YELLOW_0: 45;

        hence thesis by A4, YELLOW_3: 11;

      end;

       ex_inf_of ( {} , [:S, T:]) & {} is_>=_than [( Top S), ( Top T)] by YELLOW_0: 43;

      hence thesis by A1, YELLOW_0:def 10;

    end;

    theorem :: YELLOW10:4

    

     Th4: for S,T be lower-bounded antisymmetric non empty RelStr holds ( Bottom [:S, T:]) = [( Bottom S), ( Bottom T)]

    proof

      let S,T be lower-bounded antisymmetric non empty RelStr;

      

       A1: for a be Element of [:S, T:] st {} is_<=_than a holds [( Bottom S), ( Bottom T)] <= a

      proof

        let a be Element of [:S, T:];

        assume {} is_<=_than a;

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

        consider s,t be object such that

         A2: s in the carrier of S and

         A3: t in the carrier of T and

         A4: a = [s, t] by ZFMISC_1:def 2;

        reconsider t as Element of T by A3;

        reconsider s as Element of S by A2;

        ( Bottom S) <= s & ( Bottom T) <= t by YELLOW_0: 44;

        hence thesis by A4, YELLOW_3: 11;

      end;

       ex_sup_of ( {} , [:S, T:]) & {} is_<=_than [( Bottom S), ( Bottom T)] by YELLOW_0: 42;

      hence thesis by A1, YELLOW_0:def 9;

    end;

    theorem :: YELLOW10:5

    

     Th5: for S,T be lower-bounded antisymmetric non empty RelStr, D be Subset of [:S, T:] st [:S, T:] is complete or ex_sup_of (D, [:S, T:]) holds ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))]

    proof

      let S,T be lower-bounded antisymmetric non empty RelStr, D be Subset of [:S, T:] such that

       A1: [:S, T:] is complete or ex_sup_of (D, [:S, T:]);

      per cases ;

        suppose D <> {} ;

        hence thesis by A1, YELLOW_3: 46;

      end;

        suppose

         A2: D = {} ;

        then

         A3: ( sup ( proj2 D)) = ( Bottom T);

        ( sup D) = ( Bottom [:S, T:]) & ( sup ( proj1 D)) = ( Bottom S) by A2;

        hence thesis by A3, Th4;

      end;

    end;

    theorem :: YELLOW10:6

    for S,T be upper-bounded antisymmetric non empty RelStr, D be Subset of [:S, T:] st [:S, T:] is complete or ex_inf_of (D, [:S, T:]) holds ( inf D) = [( inf ( proj1 D)), ( inf ( proj2 D))]

    proof

      let S,T be upper-bounded antisymmetric non empty RelStr, D be Subset of [:S, T:] such that

       A1: [:S, T:] is complete or ex_inf_of (D, [:S, T:]);

      per cases ;

        suppose D <> {} ;

        hence thesis by A1, YELLOW_3: 47;

      end;

        suppose

         A2: D = {} ;

        then

         A3: ( inf ( proj2 D)) = ( Top T);

        ( inf D) = ( Top [:S, T:]) & ( inf ( proj1 D)) = ( Top S) by A2;

        hence thesis by A3, Th3;

      end;

    end;

    theorem :: YELLOW10:7

    for S,T be non empty RelStr, x,y be Element of [:S, T:] holds x is_<=_than {y} iff (x `1 ) is_<=_than {(y `1 )} & (x `2 ) is_<=_than {(y `2 )}

    proof

      let S,T be non empty RelStr, x,y be Element of [:S, T:];

      thus x is_<=_than {y} implies (x `1 ) is_<=_than {(y `1 )} & (x `2 ) is_<=_than {(y `2 )}

      proof

        

         A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

         A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

        y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

        then

         A3: [(y `1 ), (y `2 )] in {y} by TARSKI:def 1;

        assume for b be Element of [:S, T:] st b in {y} holds x <= b;

        then

         A4: x <= [(y `1 ), (y `2 )] by A3;

        hereby

          let b be Element of S;

          assume b in {(y `1 )};

          then b = (y `1 ) by TARSKI:def 1;

          hence (x `1 ) <= b by A4, A2, YELLOW_3: 11;

        end;

        let b be Element of T;

        assume b in {(y `2 )};

        then b = (y `2 ) by TARSKI:def 1;

        hence thesis by A4, A2, YELLOW_3: 11;

      end;

      assume that

       A5: for b be Element of S st b in {(y `1 )} holds (x `1 ) <= b and

       A6: for b be Element of T st b in {(y `2 )} holds (x `2 ) <= b;

      let b be Element of [:S, T:];

      assume b in {y};

      then

       A7: b = y by TARSKI:def 1;

      then (b `2 ) in {(y `2 )} by TARSKI:def 1;

      then

       A8: (x `2 ) <= (b `2 ) by A6;

      (b `1 ) in {(y `1 )} by A7, TARSKI:def 1;

      then (x `1 ) <= (b `1 ) by A5;

      hence thesis by A8, YELLOW_3: 12;

    end;

    theorem :: YELLOW10:8

    for S,T be non empty RelStr, x,y,z be Element of [:S, T:] holds x is_<=_than {y, z} iff (x `1 ) is_<=_than {(y `1 ), (z `1 )} & (x `2 ) is_<=_than {(y `2 ), (z `2 )}

    proof

      let S,T be non empty RelStr, x,y,z be Element of [:S, T:];

      thus x is_<=_than {y, z} implies (x `1 ) is_<=_than {(y `1 ), (z `1 )} & (x `2 ) is_<=_than {(y `2 ), (z `2 )}

      proof

        assume

         A1: for b be Element of [:S, T:] st b in {y, z} holds x <= b;

        

         A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then y = [(y `1 ), (y `2 )] by MCART_1: 21;

        then [(y `1 ), (y `2 )] in {y, z} by TARSKI:def 2;

        then

         A3: x <= [(y `1 ), (y `2 )] by A1;

        z = [(z `1 ), (z `2 )] by A2, MCART_1: 21;

        then [(z `1 ), (z `2 )] in {y, z} by TARSKI:def 2;

        then

         A4: x <= [(z `1 ), (z `2 )] by A1;

        

         A5: x = [(x `1 ), (x `2 )] by A2, MCART_1: 21;

        hereby

          let b be Element of S;

          assume b in {(y `1 ), (z `1 )};

          then b = (y `1 ) or b = (z `1 ) by TARSKI:def 2;

          hence (x `1 ) <= b by A3, A4, A5, YELLOW_3: 11;

        end;

        let b be Element of T;

        assume b in {(y `2 ), (z `2 )};

        then b = (y `2 ) or b = (z `2 ) by TARSKI:def 2;

        hence thesis by A3, A4, A5, YELLOW_3: 11;

      end;

      assume that

       A6: for b be Element of S st b in {(y `1 ), (z `1 )} holds (x `1 ) <= b and

       A7: for b be Element of T st b in {(y `2 ), (z `2 )} holds (x `2 ) <= b;

      let b be Element of [:S, T:];

      assume b in {y, z};

      then

       A8: b = y or b = z by TARSKI:def 2;

      then (b `2 ) in {(y `2 ), (z `2 )} by TARSKI:def 2;

      then

       A9: (x `2 ) <= (b `2 ) by A7;

      (b `1 ) in {(y `1 ), (z `1 )} by A8, TARSKI:def 2;

      then (x `1 ) <= (b `1 ) by A6;

      hence thesis by A9, YELLOW_3: 12;

    end;

    theorem :: YELLOW10:9

    for S,T be non empty RelStr, x,y be Element of [:S, T:] holds x is_>=_than {y} iff (x `1 ) is_>=_than {(y `1 )} & (x `2 ) is_>=_than {(y `2 )}

    proof

      let S,T be non empty RelStr, x,y be Element of [:S, T:];

      thus x is_>=_than {y} implies (x `1 ) is_>=_than {(y `1 )} & (x `2 ) is_>=_than {(y `2 )}

      proof

        

         A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

         A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

        y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

        then

         A3: [(y `1 ), (y `2 )] in {y} by TARSKI:def 1;

        assume for b be Element of [:S, T:] st b in {y} holds x >= b;

        then

         A4: x >= [(y `1 ), (y `2 )] by A3;

        hereby

          let b be Element of S;

          assume b in {(y `1 )};

          then b = (y `1 ) by TARSKI:def 1;

          hence (x `1 ) >= b by A4, A2, YELLOW_3: 11;

        end;

        let b be Element of T;

        assume b in {(y `2 )};

        then b = (y `2 ) by TARSKI:def 1;

        hence thesis by A4, A2, YELLOW_3: 11;

      end;

      assume that

       A5: for b be Element of S st b in {(y `1 )} holds (x `1 ) >= b and

       A6: for b be Element of T st b in {(y `2 )} holds (x `2 ) >= b;

      let b be Element of [:S, T:];

      assume b in {y};

      then

       A7: b = y by TARSKI:def 1;

      then (b `2 ) in {(y `2 )} by TARSKI:def 1;

      then

       A8: (x `2 ) >= (b `2 ) by A6;

      (b `1 ) in {(y `1 )} by A7, TARSKI:def 1;

      then (x `1 ) >= (b `1 ) by A5;

      hence thesis by A8, YELLOW_3: 12;

    end;

    theorem :: YELLOW10:10

    for S,T be non empty RelStr, x,y,z be Element of [:S, T:] holds x is_>=_than {y, z} iff (x `1 ) is_>=_than {(y `1 ), (z `1 )} & (x `2 ) is_>=_than {(y `2 ), (z `2 )}

    proof

      let S,T be non empty RelStr, x,y,z be Element of [:S, T:];

      thus x is_>=_than {y, z} implies (x `1 ) is_>=_than {(y `1 ), (z `1 )} & (x `2 ) is_>=_than {(y `2 ), (z `2 )}

      proof

        assume

         A1: for b be Element of [:S, T:] st b in {y, z} holds x >= b;

        

         A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then y = [(y `1 ), (y `2 )] by MCART_1: 21;

        then [(y `1 ), (y `2 )] in {y, z} by TARSKI:def 2;

        then

         A3: x >= [(y `1 ), (y `2 )] by A1;

        z = [(z `1 ), (z `2 )] by A2, MCART_1: 21;

        then [(z `1 ), (z `2 )] in {y, z} by TARSKI:def 2;

        then

         A4: x >= [(z `1 ), (z `2 )] by A1;

        

         A5: x = [(x `1 ), (x `2 )] by A2, MCART_1: 21;

        hereby

          let b be Element of S;

          assume b in {(y `1 ), (z `1 )};

          then b = (y `1 ) or b = (z `1 ) by TARSKI:def 2;

          hence (x `1 ) >= b by A3, A4, A5, YELLOW_3: 11;

        end;

        let b be Element of T;

        assume b in {(y `2 ), (z `2 )};

        then b = (y `2 ) or b = (z `2 ) by TARSKI:def 2;

        hence thesis by A3, A4, A5, YELLOW_3: 11;

      end;

      assume that

       A6: for b be Element of S st b in {(y `1 ), (z `1 )} holds (x `1 ) >= b and

       A7: for b be Element of T st b in {(y `2 ), (z `2 )} holds (x `2 ) >= b;

      let b be Element of [:S, T:];

      assume b in {y, z};

      then

       A8: b = y or b = z by TARSKI:def 2;

      then (b `2 ) in {(y `2 ), (z `2 )} by TARSKI:def 2;

      then

       A9: (x `2 ) >= (b `2 ) by A7;

      (b `1 ) in {(y `1 ), (z `1 )} by A8, TARSKI:def 2;

      then (x `1 ) >= (b `1 ) by A6;

      hence thesis by A9, YELLOW_3: 12;

    end;

    theorem :: YELLOW10:11

    for S,T be non empty antisymmetric RelStr, x,y be Element of [:S, T:] holds ex_inf_of ( {x, y}, [:S, T:]) iff ex_inf_of ( {(x `1 ), (y `1 )},S) & ex_inf_of ( {(x `2 ), (y `2 )},T)

    proof

      let S,T be non empty antisymmetric RelStr, x,y be Element of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] & y = [(y `1 ), (y `2 )] by MCART_1: 21;

      then ( proj1 {x, y}) = {(x `1 ), (y `1 )} & ( proj2 {x, y}) = {(x `2 ), (y `2 )} by FUNCT_5: 13;

      hence thesis by YELLOW_3: 42;

    end;

    theorem :: YELLOW10:12

    for S,T be non empty antisymmetric RelStr, x,y be Element of [:S, T:] holds ex_sup_of ( {x, y}, [:S, T:]) iff ex_sup_of ( {(x `1 ), (y `1 )},S) & ex_sup_of ( {(x `2 ), (y `2 )},T)

    proof

      let S,T be non empty antisymmetric RelStr, x,y be Element of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] & y = [(y `1 ), (y `2 )] by MCART_1: 21;

      then ( proj1 {x, y}) = {(x `1 ), (y `1 )} & ( proj2 {x, y}) = {(x `2 ), (y `2 )} by FUNCT_5: 13;

      hence thesis by YELLOW_3: 41;

    end;

    theorem :: YELLOW10:13

    

     Th13: for S,T be with_infima antisymmetric RelStr, x,y be Element of [:S, T:] holds ((x "/\" y) `1 ) = ((x `1 ) "/\" (y `1 )) & ((x "/\" y) `2 ) = ((x `2 ) "/\" (y `2 ))

    proof

      let S,T be with_infima antisymmetric RelStr, x,y be Element of [:S, T:];

      set a = ((x "/\" y) `1 ), b = ((x "/\" y) `2 );

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      

       A3: y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

      

       A4: for d be Element of S st d <= (x `1 ) & d <= (y `1 ) holds a >= d

      proof

        set t = ((x `2 ) "/\" (y `2 ));

        let d be Element of S such that

         A5: d <= (x `1 ) and

         A6: d <= (y `1 );

        t <= (y `2 ) by YELLOW_0: 23;

        then

         A7: [d, t] <= y by A3, A6, YELLOW_3: 11;

        t <= (x `2 ) by YELLOW_0: 23;

        then [d, t] <= x by A2, A5, YELLOW_3: 11;

        then

         A8: (x "/\" y) >= [d, t] by A7, YELLOW_0: 23;

        ( [d, t] `1 ) = d;

        hence thesis by A8, YELLOW_3: 12;

      end;

      

       A9: for d be Element of T st d <= (x `2 ) & d <= (y `2 ) holds b >= d

      proof

        set s = ((x `1 ) "/\" (y `1 ));

        let d be Element of T such that

         A10: d <= (x `2 ) and

         A11: d <= (y `2 );

        s <= (y `1 ) by YELLOW_0: 23;

        then

         A12: [s, d] <= y by A3, A11, YELLOW_3: 11;

        s <= (x `1 ) by YELLOW_0: 23;

        then [s, d] <= x by A2, A10, YELLOW_3: 11;

        then

         A13: (x "/\" y) >= [s, d] by A12, YELLOW_0: 23;

        ( [s, d] `2 ) = d;

        hence thesis by A13, YELLOW_3: 12;

      end;

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

      then

       A14: a <= (y `1 ) & b <= (y `2 ) by YELLOW_3: 12;

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

      then a <= (x `1 ) & b <= (x `2 ) by YELLOW_3: 12;

      hence thesis by A14, A4, A9, YELLOW_0: 19;

    end;

    theorem :: YELLOW10:14

    

     Th14: for S,T be with_suprema antisymmetric RelStr, x,y be Element of [:S, T:] holds ((x "\/" y) `1 ) = ((x `1 ) "\/" (y `1 )) & ((x "\/" y) `2 ) = ((x `2 ) "\/" (y `2 ))

    proof

      let S,T be with_suprema antisymmetric RelStr, x,y be Element of [:S, T:];

      set a = ((x "\/" y) `1 ), b = ((x "\/" y) `2 );

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      

       A3: y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

      

       A4: for d be Element of S st d >= (x `1 ) & d >= (y `1 ) holds a <= d

      proof

        set t = ((x `2 ) "\/" (y `2 ));

        let d be Element of S such that

         A5: d >= (x `1 ) and

         A6: d >= (y `1 );

        t >= (y `2 ) by YELLOW_0: 22;

        then

         A7: [d, t] >= y by A3, A6, YELLOW_3: 11;

        t >= (x `2 ) by YELLOW_0: 22;

        then [d, t] >= x by A2, A5, YELLOW_3: 11;

        then

         A8: (x "\/" y) <= [d, t] by A7, YELLOW_0: 22;

        ( [d, t] `1 ) = d;

        hence thesis by A8, YELLOW_3: 12;

      end;

      

       A9: for d be Element of T st d >= (x `2 ) & d >= (y `2 ) holds b <= d

      proof

        set s = ((x `1 ) "\/" (y `1 ));

        let d be Element of T such that

         A10: d >= (x `2 ) and

         A11: d >= (y `2 );

        s >= (y `1 ) by YELLOW_0: 22;

        then

         A12: [s, d] >= y by A3, A11, YELLOW_3: 11;

        s >= (x `1 ) by YELLOW_0: 22;

        then [s, d] >= x by A2, A10, YELLOW_3: 11;

        then

         A13: (x "\/" y) <= [s, d] by A12, YELLOW_0: 22;

        ( [s, d] `2 ) = d;

        hence thesis by A13, YELLOW_3: 12;

      end;

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

      then

       A14: a >= (y `1 ) & b >= (y `2 ) by YELLOW_3: 12;

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

      then a >= (x `1 ) & b >= (x `2 ) by YELLOW_3: 12;

      hence thesis by A14, A4, A9, YELLOW_0: 18;

    end;

    theorem :: YELLOW10:15

    

     Th15: for S,T be with_infima antisymmetric RelStr, x1,y1 be Element of S, x2,y2 be Element of T holds [(x1 "/\" y1), (x2 "/\" y2)] = ( [x1, x2] "/\" [y1, y2])

    proof

      let S,T be with_infima antisymmetric RelStr, x1,y1 be Element of S, x2,y2 be Element of T;

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      

       A2: (( [x1, x2] "/\" [y1, y2]) `2 ) = (( [x1, x2] `2 ) "/\" ( [y1, y2] `2 )) by Th13

      .= (x2 "/\" ( [y1, y2] `2 ))

      .= (x2 "/\" y2)

      .= ( [(x1 "/\" y1), (x2 "/\" y2)] `2 );

      (( [x1, x2] "/\" [y1, y2]) `1 ) = (( [x1, x2] `1 ) "/\" ( [y1, y2] `1 )) by Th13

      .= (x1 "/\" ( [y1, y2] `1 ))

      .= (x1 "/\" y1)

      .= ( [(x1 "/\" y1), (x2 "/\" y2)] `1 );

      hence thesis by A1, A2, DOMAIN_1: 2;

    end;

    theorem :: YELLOW10:16

    

     Th16: for S,T be with_suprema antisymmetric RelStr, x1,y1 be Element of S, x2,y2 be Element of T holds [(x1 "\/" y1), (x2 "\/" y2)] = ( [x1, x2] "\/" [y1, y2])

    proof

      let S,T be with_suprema antisymmetric RelStr, x1,y1 be Element of S, x2,y2 be Element of T;

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      

       A2: (( [x1, x2] "\/" [y1, y2]) `2 ) = (( [x1, x2] `2 ) "\/" ( [y1, y2] `2 )) by Th14

      .= (x2 "\/" ( [y1, y2] `2 ))

      .= (x2 "\/" y2)

      .= ( [(x1 "\/" y1), (x2 "\/" y2)] `2 );

      (( [x1, x2] "\/" [y1, y2]) `1 ) = (( [x1, x2] `1 ) "\/" ( [y1, y2] `1 )) by Th14

      .= (x1 "\/" ( [y1, y2] `1 ))

      .= (x1 "\/" y1)

      .= ( [(x1 "\/" y1), (x2 "\/" y2)] `1 );

      hence thesis by A1, A2, DOMAIN_1: 2;

    end;

    definition

      let S be with_suprema with_infima antisymmetric RelStr, x,y be Element of S;

      :: original: is_a_complement_of

      redefine

      pred y is_a_complement_of x;

      symmetry

      proof

        let a,b be Element of S;

        assume a is_a_complement_of b;

        hence (a "\/" b) = ( Top S) & (a "/\" b) = ( Bottom S);

      end;

    end

    theorem :: YELLOW10:17

    

     Th17: for S,T be bounded with_suprema with_infima antisymmetric RelStr, x,y be Element of [:S, T:] holds x is_a_complement_of y iff (x `1 ) is_a_complement_of (y `1 ) & (x `2 ) is_a_complement_of (y `2 )

    proof

      let S,T be bounded with_suprema with_infima antisymmetric RelStr, x,y be Element of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      hereby

        assume

         A2: x is_a_complement_of y;

        

         A3: ((y `1 ) "/\" (x `1 )) = ((y "/\" x) `1 ) by Th13

        .= (( Bottom [:S, T:]) `1 ) by A2

        .= ( [( Bottom S), ( Bottom T)] `1 ) by Th4

        .= ( Bottom S);

        ((y `1 ) "\/" (x `1 )) = ((y "\/" x) `1 ) by Th14

        .= (( Top [:S, T:]) `1 ) by A2

        .= ( [( Top S), ( Top T)] `1 ) by Th3

        .= ( Top S);

        hence (x `1 ) is_a_complement_of (y `1 ) by A3;

        

         A4: ((y `2 ) "/\" (x `2 )) = ((y "/\" x) `2 ) by Th13

        .= (( Bottom [:S, T:]) `2 ) by A2

        .= ( [( Bottom S), ( Bottom T)] `2 ) by Th4

        .= ( Bottom T);

        ((y `2 ) "\/" (x `2 )) = ((y "\/" x) `2 ) by Th14

        .= (( Top [:S, T:]) `2 ) by A2

        .= ( [( Top S), ( Top T)] `2 ) by Th3

        .= ( Top T);

        hence (x `2 ) is_a_complement_of (y `2 ) by A4;

      end;

      assume that

       A5: ((y `1 ) "\/" (x `1 )) = ( Top S) and

       A6: ((y `1 ) "/\" (x `1 )) = ( Bottom S) and

       A7: ((y `2 ) "\/" (x `2 )) = ( Top T) and

       A8: ((y `2 ) "/\" (x `2 )) = ( Bottom T);

      

       A9: ((y "\/" x) `2 ) = ((y `2 ) "\/" (x `2 )) by Th14

      .= ( [( Top S), ( Top T)] `2 ) by A7;

      ((y "\/" x) `1 ) = ((y `1 ) "\/" (x `1 )) by Th14

      .= ( [( Top S), ( Top T)] `1 ) by A5;

      

      hence (y "\/" x) = [( Top S), ( Top T)] by A1, A9, DOMAIN_1: 2

      .= ( Top [:S, T:]) by Th3;

      

       A10: ((y "/\" x) `2 ) = ((y `2 ) "/\" (x `2 )) by Th13

      .= ( [( Bottom S), ( Bottom T)] `2 ) by A8;

      ((y "/\" x) `1 ) = ((y `1 ) "/\" (x `1 )) by Th13

      .= ( [( Bottom S), ( Bottom T)] `1 ) by A6;

      

      hence (y "/\" x) = [( Bottom S), ( Bottom T)] by A1, A10, DOMAIN_1: 2

      .= ( Bottom [:S, T:]) by Th4;

    end;

    theorem :: YELLOW10:18

    

     Th18: for S,T be antisymmetric up-complete non empty reflexive RelStr, a,c be Element of S, b,d be Element of T st [a, b] << [c, d] holds a << c & b << d

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, a,c be Element of S, b,d be Element of T;

      assume

       A1: for D be non empty directed Subset of [:S, T:] st [c, d] <= ( sup D) holds ex e be Element of [:S, T:] st e in D & [a, b] <= e;

      

       A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      thus a << c

      proof

        reconsider d9 = {d} as non empty directed Subset of T by WAYBEL_0: 5;

        let D be non empty directed Subset of S such that

         A3: c <= ( sup D);

        

         A4: d <= ( sup d9) by YELLOW_0: 39;

         ex_sup_of (D,S) & ex_sup_of (d9,T) by WAYBEL_0: 75;

        then ( sup [:D, d9:]) = [( sup D), ( sup d9)] by YELLOW_3: 43;

        then [c, d] <= ( sup [:D, d9:]) by A3, A4, YELLOW_3: 11;

        then

        consider e be Element of [:S, T:] such that

         A5: e in [:D, d9:] and

         A6: [a, b] <= e by A1;

        take (e `1 );

        thus (e `1 ) in D by A5, MCART_1: 10;

        e = [(e `1 ), (e `2 )] by A2, MCART_1: 21;

        hence thesis by A6, YELLOW_3: 11;

      end;

      let D be non empty directed Subset of T such that

       A7: d <= ( sup D);

      reconsider c9 = {c} as non empty directed Subset of S by WAYBEL_0: 5;

      

       A8: c <= ( sup c9) by YELLOW_0: 39;

       ex_sup_of (c9,S) & ex_sup_of (D,T) by WAYBEL_0: 75;

      then ( sup [:c9, D:]) = [( sup c9), ( sup D)] by YELLOW_3: 43;

      then [c, d] <= ( sup [:c9, D:]) by A7, A8, YELLOW_3: 11;

      then

      consider e be Element of [:S, T:] such that

       A9: e in [:c9, D:] and

       A10: [a, b] <= e by A1;

      take (e `2 );

      thus (e `2 ) in D by A9, MCART_1: 10;

      e = [(e `1 ), (e `2 )] by A2, MCART_1: 21;

      hence thesis by A10, YELLOW_3: 11;

    end;

    theorem :: YELLOW10:19

    

     Th19: for S,T be up-complete non empty Poset holds for a,c be Element of S, b,d be Element of T holds [a, b] << [c, d] iff a << c & b << d

    proof

      let S,T be up-complete non empty Poset, a,c be Element of S, b,d be Element of T;

      thus [a, b] << [c, d] implies a << c & b << d by Th18;

      assume

       A1: for D be non empty directed Subset of S st c <= ( sup D) holds ex e be Element of S st e in D & a <= e;

      assume

       A2: for D be non empty directed Subset of T st d <= ( sup D) holds ex e be Element of T st e in D & b <= e;

      let D be non empty directed Subset of [:S, T:] such that

       A3: [c, d] <= ( sup D);

       ex_sup_of (D, [:S, T:]) by WAYBEL_0: 75;

      then

       A4: ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))] by YELLOW_3: 46;

      then ( proj1 D) is non empty directed & c <= ( sup ( proj1 D)) by A3, YELLOW_3: 11, YELLOW_3: 21, YELLOW_3: 22;

      then

      consider e be Element of S such that

       A5: e in ( proj1 D) and

       A6: a <= e by A1;

      consider e2 be object such that

       A7: [e, e2] in D by A5, XTUPLE_0:def 12;

      ( proj2 D) is non empty directed & d <= ( sup ( proj2 D)) by A3, A4, YELLOW_3: 11, YELLOW_3: 21, YELLOW_3: 22;

      then

      consider f be Element of T such that

       A8: f in ( proj2 D) and

       A9: b <= f by A2;

      consider f1 be object such that

       A10: [f1, f] in D by A8, XTUPLE_0:def 13;

      

       A11: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider e2 as Element of T by A7, ZFMISC_1: 87;

      reconsider f1 as Element of S by A11, A10, ZFMISC_1: 87;

      consider ef be Element of [:S, T:] such that

       A12: ef in D and

       A13: [e, e2] <= ef & [f1, f] <= ef by A7, A10, WAYBEL_0:def 1;

      

       A14: ef = [(ef `1 ), (ef `2 )] by A11, MCART_1: 21;

      then e <= (ef `1 ) & f <= (ef `2 ) by A13, YELLOW_3: 11;

      then

       A15: [e, f] <= ef by A14, YELLOW_3: 11;

      take ef;

      thus ef in D by A12;

       [a, b] <= [e, f] by A6, A9, YELLOW_3: 11;

      hence thesis by A15, ORDERS_2: 3;

    end;

    theorem :: YELLOW10:20

    

     Th20: for S,T be antisymmetric up-complete non empty reflexive RelStr, x,y be Element of [:S, T:] st x << y holds (x `1 ) << (y `1 ) & (x `2 ) << (y `2 )

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, x,y be Element of [:S, T:] such that

       A1: x << y;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] & y = [(y `1 ), (y `2 )] by MCART_1: 21;

      hence thesis by A1, Th18;

    end;

    theorem :: YELLOW10:21

    

     Th21: for S,T be up-complete non empty Poset, x,y be Element of [:S, T:] holds x << y iff (x `1 ) << (y `1 ) & (x `2 ) << (y `2 )

    proof

      let S,T be up-complete non empty Poset, x,y be Element of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] & y = [(y `1 ), (y `2 )] by MCART_1: 21;

      hence thesis by Th19;

    end;

    theorem :: YELLOW10:22

    

     Th22: for S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:] st x is compact holds (x `1 ) is compact & (x `2 ) is compact

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:];

      assume

       A1: x << x;

      hence (x `1 ) << (x `1 ) by Th20;

      thus (x `2 ) << (x `2 ) by A1, Th20;

    end;

    theorem :: YELLOW10:23

    

     Th23: for S,T be up-complete non empty Poset, x be Element of [:S, T:] st (x `1 ) is compact & (x `2 ) is compact holds x is compact

    proof

      let S,T be up-complete non empty Poset, x be Element of [:S, T:];

      assume (x `1 ) << (x `1 ) & (x `2 ) << (x `2 );

      hence x << x by Th21;

    end;

    begin

    theorem :: YELLOW10:24

    

     Th24: for S,T be with_infima antisymmetric RelStr, X,Y be Subset of [:S, T:] holds ( proj1 (X "/\" Y)) = (( proj1 X) "/\" ( proj1 Y)) & ( proj2 (X "/\" Y)) = (( proj2 X) "/\" ( proj2 Y))

    proof

      let S,T be with_infima antisymmetric RelStr, X,Y be Subset of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      

       A2: (X "/\" Y) = { (x "/\" y) where x,y be Element of [:S, T:] : x in X & y in Y } by YELLOW_4:def 4;

      

       A3: (( proj1 X) "/\" ( proj1 Y)) = { (x "/\" y) where x,y be Element of S : x in ( proj1 X) & y in ( proj1 Y) } by YELLOW_4:def 4;

      hereby

        hereby

          let a be object;

          assume a in ( proj1 (X "/\" Y));

          then

          consider b be object such that

           A4: [a, b] in (X "/\" Y) by XTUPLE_0:def 12;

          consider x,y be Element of [:S, T:] such that

           A5: [a, b] = (x "/\" y) and

           A6: x in X and

           A7: y in Y by A2, A4;

          x = [(x `1 ), (x `2 )] by A1, MCART_1: 21;

          then

           A8: (x `1 ) in ( proj1 X) by A6, XTUPLE_0:def 12;

          y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

          then

           A9: (y `1 ) in ( proj1 Y) by A7, XTUPLE_0:def 12;

          a = ( [a, b] `1 )

          .= ((x `1 ) "/\" (y `1 )) by A5, Th13;

          hence a in (( proj1 X) "/\" ( proj1 Y)) by A8, A9, YELLOW_4: 37;

        end;

        let a be object;

        assume a in (( proj1 X) "/\" ( proj1 Y));

        then

        consider x,y be Element of S such that

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

         A11: x in ( proj1 X) and

         A12: y in ( proj1 Y) by A3;

        consider x2 be object such that

         A13: [x, x2] in X by A11, XTUPLE_0:def 12;

        consider y2 be object such that

         A14: [y, y2] in Y by A12, XTUPLE_0:def 12;

        reconsider x2, y2 as Element of T by A1, A13, A14, ZFMISC_1: 87;

        ( [x, x2] "/\" [y, y2]) = [a, (x2 "/\" y2)] by A10, Th15;

        then [a, (x2 "/\" y2)] in (X "/\" Y) by A13, A14, YELLOW_4: 37;

        hence a in ( proj1 (X "/\" Y)) by XTUPLE_0:def 12;

      end;

      hereby

        let b be object;

        assume b in ( proj2 (X "/\" Y));

        then

        consider a be object such that

         A15: [a, b] in (X "/\" Y) by XTUPLE_0:def 13;

        consider x,y be Element of [:S, T:] such that

         A16: [a, b] = (x "/\" y) and

         A17: x in X and

         A18: y in Y by A2, A15;

        x = [(x `1 ), (x `2 )] by A1, MCART_1: 21;

        then

         A19: (x `2 ) in ( proj2 X) by A17, XTUPLE_0:def 13;

        y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

        then

         A20: (y `2 ) in ( proj2 Y) by A18, XTUPLE_0:def 13;

        b = ( [a, b] `2 )

        .= ((x `2 ) "/\" (y `2 )) by A16, Th13;

        hence b in (( proj2 X) "/\" ( proj2 Y)) by A19, A20, YELLOW_4: 37;

      end;

      let b be object;

      

       A21: (( proj2 X) "/\" ( proj2 Y)) = { (x "/\" y) where x,y be Element of T : x in ( proj2 X) & y in ( proj2 Y) } by YELLOW_4:def 4;

      assume b in (( proj2 X) "/\" ( proj2 Y));

      then

      consider x,y be Element of T such that

       A22: b = (x "/\" y) and

       A23: x in ( proj2 X) and

       A24: y in ( proj2 Y) by A21;

      consider x1 be object such that

       A25: [x1, x] in X by A23, XTUPLE_0:def 13;

      consider y1 be object such that

       A26: [y1, y] in Y by A24, XTUPLE_0:def 13;

      reconsider x1, y1 as Element of S by A1, A25, A26, ZFMISC_1: 87;

      ( [x1, x] "/\" [y1, y]) = [(x1 "/\" y1), b] by A22, Th15;

      then [(x1 "/\" y1), b] in (X "/\" Y) by A25, A26, YELLOW_4: 37;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:25

    for S,T be with_suprema antisymmetric RelStr, X,Y be Subset of [:S, T:] holds ( proj1 (X "\/" Y)) = (( proj1 X) "\/" ( proj1 Y)) & ( proj2 (X "\/" Y)) = (( proj2 X) "\/" ( proj2 Y))

    proof

      let S,T be with_suprema antisymmetric RelStr, X,Y be Subset of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      

       A2: (X "\/" Y) = { (x "\/" y) where x,y be Element of [:S, T:] : x in X & y in Y } by YELLOW_4:def 3;

      

       A3: (( proj1 X) "\/" ( proj1 Y)) = { (x "\/" y) where x,y be Element of S : x in ( proj1 X) & y in ( proj1 Y) } by YELLOW_4:def 3;

      hereby

        hereby

          let a be object;

          assume a in ( proj1 (X "\/" Y));

          then

          consider b be object such that

           A4: [a, b] in (X "\/" Y) by XTUPLE_0:def 12;

          consider x,y be Element of [:S, T:] such that

           A5: [a, b] = (x "\/" y) and

           A6: x in X and

           A7: y in Y by A2, A4;

          x = [(x `1 ), (x `2 )] by A1, MCART_1: 21;

          then

           A8: (x `1 ) in ( proj1 X) by A6, XTUPLE_0:def 12;

          y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

          then

           A9: (y `1 ) in ( proj1 Y) by A7, XTUPLE_0:def 12;

          a = ( [a, b] `1 )

          .= ((x `1 ) "\/" (y `1 )) by A5, Th14;

          hence a in (( proj1 X) "\/" ( proj1 Y)) by A8, A9, YELLOW_4: 10;

        end;

        let a be object;

        assume a in (( proj1 X) "\/" ( proj1 Y));

        then

        consider x,y be Element of S such that

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

         A11: x in ( proj1 X) and

         A12: y in ( proj1 Y) by A3;

        consider x2 be object such that

         A13: [x, x2] in X by A11, XTUPLE_0:def 12;

        consider y2 be object such that

         A14: [y, y2] in Y by A12, XTUPLE_0:def 12;

        reconsider x2, y2 as Element of T by A1, A13, A14, ZFMISC_1: 87;

        ( [x, x2] "\/" [y, y2]) = [a, (x2 "\/" y2)] by A10, Th16;

        then [a, (x2 "\/" y2)] in (X "\/" Y) by A13, A14, YELLOW_4: 10;

        hence a in ( proj1 (X "\/" Y)) by XTUPLE_0:def 12;

      end;

      hereby

        let b be object;

        assume b in ( proj2 (X "\/" Y));

        then

        consider a be object such that

         A15: [a, b] in (X "\/" Y) by XTUPLE_0:def 13;

        consider x,y be Element of [:S, T:] such that

         A16: [a, b] = (x "\/" y) and

         A17: x in X and

         A18: y in Y by A2, A15;

        x = [(x `1 ), (x `2 )] by A1, MCART_1: 21;

        then

         A19: (x `2 ) in ( proj2 X) by A17, XTUPLE_0:def 13;

        y = [(y `1 ), (y `2 )] by A1, MCART_1: 21;

        then

         A20: (y `2 ) in ( proj2 Y) by A18, XTUPLE_0:def 13;

        b = ( [a, b] `2 )

        .= ((x `2 ) "\/" (y `2 )) by A16, Th14;

        hence b in (( proj2 X) "\/" ( proj2 Y)) by A19, A20, YELLOW_4: 10;

      end;

      let b be object;

      

       A21: (( proj2 X) "\/" ( proj2 Y)) = { (x "\/" y) where x,y be Element of T : x in ( proj2 X) & y in ( proj2 Y) } by YELLOW_4:def 3;

      assume b in (( proj2 X) "\/" ( proj2 Y));

      then

      consider x,y be Element of T such that

       A22: b = (x "\/" y) and

       A23: x in ( proj2 X) and

       A24: y in ( proj2 Y) by A21;

      consider x1 be object such that

       A25: [x1, x] in X by A23, XTUPLE_0:def 13;

      consider y1 be object such that

       A26: [y1, y] in Y by A24, XTUPLE_0:def 13;

      reconsider x1, y1 as Element of S by A1, A25, A26, ZFMISC_1: 87;

      ( [x1, x] "\/" [y1, y]) = [(x1 "\/" y1), b] by A22, Th16;

      then [(x1 "\/" y1), b] in (X "\/" Y) by A25, A26, YELLOW_4: 10;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:26

    for S,T be RelStr, X be Subset of [:S, T:] holds ( downarrow X) c= [:( downarrow ( proj1 X)), ( downarrow ( proj2 X)):]

    proof

      let S,T be RelStr, X be Subset of [:S, T:];

      let x be object;

      assume

       A1: x in ( downarrow X);

      

       A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then ex a,b be object st a in the carrier of S & b in the carrier of T & x = [a, b] by A1, ZFMISC_1:def 2;

      then

      reconsider S9 = S, T9 = T as non empty RelStr;

      reconsider x9 = x as Element of [:S9, T9:] by A1;

      consider y be Element of [:S9, T9:] such that

       A3: y >= x9 and

       A4: y in X by A1, WAYBEL_0:def 15;

      

       A5: (y `1 ) >= (x9 `1 ) by A3, YELLOW_3: 12;

      

       A6: y = [(y `1 ), (y `2 )] by A2, MCART_1: 21;

      then (y `1 ) in ( proj1 X) by A4, XTUPLE_0:def 12;

      then

       A7: (x `1 ) in ( downarrow ( proj1 X)) by A5, WAYBEL_0:def 15;

      

       A8: (y `2 ) >= (x9 `2 ) by A3, YELLOW_3: 12;

      (y `2 ) in ( proj2 X) by A4, A6, XTUPLE_0:def 13;

      then

       A9: (x `2 ) in ( downarrow ( proj2 X)) by A8, WAYBEL_0:def 15;

      x9 = [(x9 `1 ), (x9 `2 )] by A2, MCART_1: 21;

      hence thesis by A7, A9, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:27

    for S,T be RelStr, X be Subset of S, Y be Subset of T holds [:( downarrow X), ( downarrow Y):] = ( downarrow [:X, Y:])

    proof

      let S,T be RelStr, X be Subset of S, Y be Subset of T;

      hereby

        let x be object;

        assume x in [:( downarrow X), ( downarrow Y):];

        then

        consider x1,x2 be object such that

         A1: x1 in ( downarrow X) and

         A2: x2 in ( downarrow Y) and

         A3: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider S9 = S, T9 = T as non empty RelStr by A1, A2;

        reconsider x1 as Element of S9 by A1;

        consider y1 be Element of S9 such that

         A4: y1 >= x1 & y1 in X by A1, WAYBEL_0:def 15;

        reconsider x2 as Element of T9 by A2;

        consider y2 be Element of T9 such that

         A5: y2 >= x2 & y2 in Y by A2, WAYBEL_0:def 15;

         [y1, y2] in [:X, Y:] & [y1, y2] >= [x1, x2] by A4, A5, YELLOW_3: 11, ZFMISC_1: 87;

        hence x in ( downarrow [:X, Y:]) by A3, WAYBEL_0:def 15;

      end;

      let x be object;

      assume

       A6: x in ( downarrow [:X, Y:]);

      

       A7: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then ex a,b be object st a in the carrier of S & b in the carrier of T & x = [a, b] by A6, ZFMISC_1:def 2;

      then

      reconsider S9 = S, T9 = T as non empty RelStr;

      reconsider x9 = x as Element of [:S9, T9:] by A6;

      consider y be Element of [:S9, T9:] such that

       A8: y >= x9 & y in [:X, Y:] by A6, WAYBEL_0:def 15;

      (y `2 ) >= (x9 `2 ) & (y `2 ) in Y by A8, MCART_1: 10, YELLOW_3: 12;

      then

       A9: (x `2 ) in ( downarrow Y) by WAYBEL_0:def 15;

      (y `1 ) >= (x9 `1 ) & (y `1 ) in X by A8, MCART_1: 10, YELLOW_3: 12;

      then

       A10: (x `1 ) in ( downarrow X) by WAYBEL_0:def 15;

      x9 = [(x9 `1 ), (x9 `2 )] by A7, MCART_1: 21;

      hence thesis by A10, A9, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:28

    

     Th28: for S,T be RelStr, X be Subset of [:S, T:] holds ( proj1 ( downarrow X)) c= ( downarrow ( proj1 X)) & ( proj2 ( downarrow X)) c= ( downarrow ( proj2 X))

    proof

      let S,T be RelStr, X be Subset of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      hereby

        let a be object;

        assume a in ( proj1 ( downarrow X));

        then

        consider b be object such that

         A2: [a, b] in ( downarrow X) by XTUPLE_0:def 12;

        reconsider S9 = S, T9 = T as non empty RelStr by A1, A2, ZFMISC_1: 87;

        reconsider b9 = b as Element of T9 by A1, A2, ZFMISC_1: 87;

        reconsider a9 = a as Element of S9 by A1, A2, ZFMISC_1: 87;

        consider c be Element of [:S9, T9:] such that

         A3: [a9, b9] <= c & c in X by A2, WAYBEL_0:def 15;

        c = [(c `1 ), (c `2 )] by A1, MCART_1: 21;

        then a9 <= (c `1 ) & (c `1 ) in ( proj1 X) by A3, XTUPLE_0:def 12, YELLOW_3: 11;

        hence a in ( downarrow ( proj1 X)) by WAYBEL_0:def 15;

      end;

      let b be object;

      assume b in ( proj2 ( downarrow X));

      then

      consider a be object such that

       A4: [a, b] in ( downarrow X) by XTUPLE_0:def 13;

      reconsider S9 = S, T9 = T as non empty RelStr by A1, A4, ZFMISC_1: 87;

      reconsider b9 = b as Element of T9 by A1, A4, ZFMISC_1: 87;

      reconsider a9 = a as Element of S9 by A1, A4, ZFMISC_1: 87;

      consider c be Element of [:S9, T9:] such that

       A5: [a9, b9] <= c & c in X by A4, WAYBEL_0:def 15;

      c = [(c `1 ), (c `2 )] by A1, MCART_1: 21;

      then b9 <= (c `2 ) & (c `2 ) in ( proj2 X) by A5, XTUPLE_0:def 13, YELLOW_3: 11;

      hence thesis by WAYBEL_0:def 15;

    end;

    theorem :: YELLOW10:29

    for S be RelStr, T be reflexive RelStr, X be Subset of [:S, T:] holds ( proj1 ( downarrow X)) = ( downarrow ( proj1 X))

    proof

      let S be RelStr, T be reflexive RelStr, X be Subset of [:S, T:];

      thus ( proj1 ( downarrow X)) c= ( downarrow ( proj1 X)) by Th28;

      let a be object;

      assume

       A1: a in ( downarrow ( proj1 X));

      then

      reconsider S9 = S as non empty RelStr;

      reconsider a9 = a as Element of S9 by A1;

      consider b be Element of S9 such that

       A2: b >= a9 and

       A3: b in ( proj1 X) by A1, WAYBEL_0:def 15;

      consider b2 be object such that

       A4: [b, b2] in X by A3, XTUPLE_0:def 12;

      

       A5: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider T9 = T as non empty reflexive RelStr by A4, ZFMISC_1: 87;

      reconsider b2 as Element of T9 by A5, A4, ZFMISC_1: 87;

      b2 <= b2;

      then [b, b2] >= [a9, b2] by A2, YELLOW_3: 11;

      then [a9, b2] in ( downarrow X) by A4, WAYBEL_0:def 15;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: YELLOW10:30

    for S be reflexive RelStr, T be RelStr, X be Subset of [:S, T:] holds ( proj2 ( downarrow X)) = ( downarrow ( proj2 X))

    proof

      let S be reflexive RelStr, T be RelStr, X be Subset of [:S, T:];

      thus ( proj2 ( downarrow X)) c= ( downarrow ( proj2 X)) by Th28;

      let c be object;

      assume

       A1: c in ( downarrow ( proj2 X));

      then

      reconsider T9 = T as non empty RelStr;

      reconsider c9 = c as Element of T9 by A1;

      consider b be Element of T9 such that

       A2: b >= c9 and

       A3: b in ( proj2 X) by A1, WAYBEL_0:def 15;

      consider b1 be object such that

       A4: [b1, b] in X by A3, XTUPLE_0:def 13;

      

       A5: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider S9 = S as non empty reflexive RelStr by A4, ZFMISC_1: 87;

      reconsider b1 as Element of S9 by A5, A4, ZFMISC_1: 87;

      b1 <= b1;

      then [b1, b] >= [b1, c9] by A2, YELLOW_3: 11;

      then [b1, c9] in ( downarrow X) by A4, WAYBEL_0:def 15;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:31

    for S,T be RelStr, X be Subset of [:S, T:] holds ( uparrow X) c= [:( uparrow ( proj1 X)), ( uparrow ( proj2 X)):]

    proof

      let S,T be RelStr, X be Subset of [:S, T:];

      let x be object;

      assume

       A1: x in ( uparrow X);

      

       A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then ex a,b be object st a in the carrier of S & b in the carrier of T & x = [a, b] by A1, ZFMISC_1:def 2;

      then

      reconsider S9 = S, T9 = T as non empty RelStr;

      reconsider x9 = x as Element of [:S9, T9:] by A1;

      consider y be Element of [:S9, T9:] such that

       A3: y <= x9 and

       A4: y in X by A1, WAYBEL_0:def 16;

      

       A5: (y `1 ) <= (x9 `1 ) by A3, YELLOW_3: 12;

      

       A6: y = [(y `1 ), (y `2 )] by A2, MCART_1: 21;

      then (y `1 ) in ( proj1 X) by A4, XTUPLE_0:def 12;

      then

       A7: (x `1 ) in ( uparrow ( proj1 X)) by A5, WAYBEL_0:def 16;

      

       A8: (y `2 ) <= (x9 `2 ) by A3, YELLOW_3: 12;

      (y `2 ) in ( proj2 X) by A4, A6, XTUPLE_0:def 13;

      then

       A9: (x `2 ) in ( uparrow ( proj2 X)) by A8, WAYBEL_0:def 16;

      x9 = [(x9 `1 ), (x9 `2 )] by A2, MCART_1: 21;

      hence thesis by A7, A9, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:32

    for S,T be RelStr, X be Subset of S, Y be Subset of T holds [:( uparrow X), ( uparrow Y):] = ( uparrow [:X, Y:])

    proof

      let S,T be RelStr, X be Subset of S, Y be Subset of T;

      hereby

        let x be object;

        assume x in [:( uparrow X), ( uparrow Y):];

        then

        consider x1,x2 be object such that

         A1: x1 in ( uparrow X) and

         A2: x2 in ( uparrow Y) and

         A3: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider S9 = S, T9 = T as non empty RelStr by A1, A2;

        reconsider x1 as Element of S9 by A1;

        consider y1 be Element of S9 such that

         A4: y1 <= x1 & y1 in X by A1, WAYBEL_0:def 16;

        reconsider x2 as Element of T9 by A2;

        consider y2 be Element of T9 such that

         A5: y2 <= x2 & y2 in Y by A2, WAYBEL_0:def 16;

         [y1, y2] in [:X, Y:] & [y1, y2] <= [x1, x2] by A4, A5, YELLOW_3: 11, ZFMISC_1: 87;

        hence x in ( uparrow [:X, Y:]) by A3, WAYBEL_0:def 16;

      end;

      let x be object;

      assume

       A6: x in ( uparrow [:X, Y:]);

      

       A7: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then ex a,b be object st a in the carrier of S & b in the carrier of T & x = [a, b] by A6, ZFMISC_1:def 2;

      then

      reconsider S9 = S, T9 = T as non empty RelStr;

      reconsider x9 = x as Element of [:S9, T9:] by A6;

      consider y be Element of [:S9, T9:] such that

       A8: y <= x9 & y in [:X, Y:] by A6, WAYBEL_0:def 16;

      (y `2 ) <= (x9 `2 ) & (y `2 ) in Y by A8, MCART_1: 10, YELLOW_3: 12;

      then

       A9: (x `2 ) in ( uparrow Y) by WAYBEL_0:def 16;

      (y `1 ) <= (x9 `1 ) & (y `1 ) in X by A8, MCART_1: 10, YELLOW_3: 12;

      then

       A10: (x `1 ) in ( uparrow X) by WAYBEL_0:def 16;

      x9 = [(x9 `1 ), (x9 `2 )] by A7, MCART_1: 21;

      hence thesis by A10, A9, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:33

    

     Th33: for S,T be RelStr, X be Subset of [:S, T:] holds ( proj1 ( uparrow X)) c= ( uparrow ( proj1 X)) & ( proj2 ( uparrow X)) c= ( uparrow ( proj2 X))

    proof

      let S,T be RelStr, X be Subset of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      hereby

        let a be object;

        assume a in ( proj1 ( uparrow X));

        then

        consider b be object such that

         A2: [a, b] in ( uparrow X) by XTUPLE_0:def 12;

        reconsider S9 = S, T9 = T as non empty RelStr by A1, A2, ZFMISC_1: 87;

        reconsider b9 = b as Element of T9 by A1, A2, ZFMISC_1: 87;

        reconsider a9 = a as Element of S9 by A1, A2, ZFMISC_1: 87;

        consider c be Element of [:S9, T9:] such that

         A3: [a9, b9] >= c & c in X by A2, WAYBEL_0:def 16;

        c = [(c `1 ), (c `2 )] by A1, MCART_1: 21;

        then a9 >= (c `1 ) & (c `1 ) in ( proj1 X) by A3, XTUPLE_0:def 12, YELLOW_3: 11;

        hence a in ( uparrow ( proj1 X)) by WAYBEL_0:def 16;

      end;

      let b be object;

      assume b in ( proj2 ( uparrow X));

      then

      consider a be object such that

       A4: [a, b] in ( uparrow X) by XTUPLE_0:def 13;

      reconsider S9 = S, T9 = T as non empty RelStr by A1, A4, ZFMISC_1: 87;

      reconsider b9 = b as Element of T9 by A1, A4, ZFMISC_1: 87;

      reconsider a9 = a as Element of S9 by A1, A4, ZFMISC_1: 87;

      consider c be Element of [:S9, T9:] such that

       A5: [a9, b9] >= c & c in X by A4, WAYBEL_0:def 16;

      c = [(c `1 ), (c `2 )] by A1, MCART_1: 21;

      then b9 >= (c `2 ) & (c `2 ) in ( proj2 X) by A5, XTUPLE_0:def 13, YELLOW_3: 11;

      hence thesis by WAYBEL_0:def 16;

    end;

    theorem :: YELLOW10:34

    for S be RelStr, T be reflexive RelStr, X be Subset of [:S, T:] holds ( proj1 ( uparrow X)) = ( uparrow ( proj1 X))

    proof

      let S be RelStr, T be reflexive RelStr, X be Subset of [:S, T:];

      thus ( proj1 ( uparrow X)) c= ( uparrow ( proj1 X)) by Th33;

      let a be object;

      assume

       A1: a in ( uparrow ( proj1 X));

      then

      reconsider S9 = S as non empty RelStr;

      reconsider a9 = a as Element of S9 by A1;

      consider b be Element of S9 such that

       A2: b <= a9 and

       A3: b in ( proj1 X) by A1, WAYBEL_0:def 16;

      consider b2 be object such that

       A4: [b, b2] in X by A3, XTUPLE_0:def 12;

      

       A5: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider T9 = T as non empty reflexive RelStr by A4, ZFMISC_1: 87;

      reconsider b2 as Element of T9 by A5, A4, ZFMISC_1: 87;

      b2 <= b2;

      then [b, b2] <= [a9, b2] by A2, YELLOW_3: 11;

      then [a9, b2] in ( uparrow X) by A4, WAYBEL_0:def 16;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: YELLOW10:35

    for S be reflexive RelStr, T be RelStr, X be Subset of [:S, T:] holds ( proj2 ( uparrow X)) = ( uparrow ( proj2 X))

    proof

      let S be reflexive RelStr, T be RelStr, X be Subset of [:S, T:];

      thus ( proj2 ( uparrow X)) c= ( uparrow ( proj2 X)) by Th33;

      let c be object;

      assume

       A1: c in ( uparrow ( proj2 X));

      then

      reconsider T9 = T as non empty RelStr;

      reconsider c9 = c as Element of T9 by A1;

      consider b be Element of T9 such that

       A2: b <= c9 and

       A3: b in ( proj2 X) by A1, WAYBEL_0:def 16;

      consider b1 be object such that

       A4: [b1, b] in X by A3, XTUPLE_0:def 13;

      

       A5: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider S9 = S as non empty reflexive RelStr by A4, ZFMISC_1: 87;

      reconsider b1 as Element of S9 by A5, A4, ZFMISC_1: 87;

      b1 <= b1;

      then [b1, b] <= [b1, c9] by A2, YELLOW_3: 11;

      then [b1, c9] in ( uparrow X) by A4, WAYBEL_0:def 16;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:36

    for S,T be non empty RelStr, s be Element of S, t be Element of T holds [:( downarrow s), ( downarrow t):] = ( downarrow [s, t])

    proof

      let S,T be non empty RelStr, s be Element of S, t be Element of T;

      hereby

        let x be object;

        assume x in [:( downarrow s), ( downarrow t):];

        then

        consider x1,x2 be object such that

         A1: x1 in ( downarrow s) and

         A2: x2 in ( downarrow t) and

         A3: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x2 as Element of T by A2;

        reconsider x1 as Element of S by A1;

        s >= x1 & t >= x2 by A1, A2, WAYBEL_0: 17;

        then [s, t] >= [x1, x2] by YELLOW_3: 11;

        hence x in ( downarrow [s, t]) by A3, WAYBEL_0: 17;

      end;

      let x be object;

      assume

       A4: x in ( downarrow [s, t]);

      then

      reconsider x9 = x as Element of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A5: x9 = [(x9 `1 ), (x9 `2 )] by MCART_1: 21;

      

       A6: [s, t] >= x9 by A4, WAYBEL_0: 17;

      then t >= (x9 `2 ) by A5, YELLOW_3: 11;

      then

       A7: (x `2 ) in ( downarrow t) by WAYBEL_0: 17;

      s >= (x9 `1 ) by A5, A6, YELLOW_3: 11;

      then (x `1 ) in ( downarrow s) by WAYBEL_0: 17;

      hence thesis by A5, A7, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:37

    

     Th37: for S,T be non empty RelStr, x be Element of [:S, T:] holds ( proj1 ( downarrow x)) c= ( downarrow (x `1 )) & ( proj2 ( downarrow x)) c= ( downarrow (x `2 ))

    proof

      let S,T be non empty RelStr, x be Element of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hereby

        let a be object;

        assume a in ( proj1 ( downarrow x));

        then

        consider b be object such that

         A3: [a, b] in ( downarrow x) by XTUPLE_0:def 12;

        reconsider b as Element of T by A1, A3, ZFMISC_1: 87;

        reconsider a9 = a as Element of S by A1, A3, ZFMISC_1: 87;

         [a9, b] <= x by A3, WAYBEL_0: 17;

        then a9 <= (x `1 ) by A2, YELLOW_3: 11;

        hence a in ( downarrow (x `1 )) by WAYBEL_0: 17;

      end;

      let b be object;

      assume b in ( proj2 ( downarrow x));

      then

      consider a be object such that

       A4: [a, b] in ( downarrow x) by XTUPLE_0:def 13;

      reconsider a as Element of S by A1, A4, ZFMISC_1: 87;

      reconsider b9 = b as Element of T by A1, A4, ZFMISC_1: 87;

       [a, b9] <= x by A4, WAYBEL_0: 17;

      then b9 <= (x `2 ) by A2, YELLOW_3: 11;

      hence thesis by WAYBEL_0: 17;

    end;

    theorem :: YELLOW10:38

    for S be non empty RelStr, T be non empty reflexive RelStr, x be Element of [:S, T:] holds ( proj1 ( downarrow x)) = ( downarrow (x `1 ))

    proof

      let S be non empty RelStr, T be non empty reflexive RelStr, x be Element of [:S, T:];

      

       A1: (x `2 ) <= (x `2 );

      thus ( proj1 ( downarrow x)) c= ( downarrow (x `1 )) by Th37;

      let a be object;

      assume

       A2: a in ( downarrow (x `1 ));

      then

      reconsider a9 = a as Element of S;

      a9 <= (x `1 ) by A2, WAYBEL_0: 17;

      then [a9, (x `2 )] <= [(x `1 ), (x `2 )] by A1, YELLOW_3: 11;

      then

       A3: [a9, (x `2 )] in ( downarrow [(x `1 ), (x `2 )]) by WAYBEL_0: 17;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hence thesis by A3, XTUPLE_0:def 12;

    end;

    theorem :: YELLOW10:39

    for S be non empty reflexive RelStr, T be non empty RelStr, x be Element of [:S, T:] holds ( proj2 ( downarrow x)) = ( downarrow (x `2 ))

    proof

      let S be non empty reflexive RelStr, T be non empty RelStr, x be Element of [:S, T:];

      

       A1: (x `1 ) <= (x `1 );

      thus ( proj2 ( downarrow x)) c= ( downarrow (x `2 )) by Th37;

      let b be object;

      assume

       A2: b in ( downarrow (x `2 ));

      then

      reconsider b9 = b as Element of T;

      b9 <= (x `2 ) by A2, WAYBEL_0: 17;

      then [(x `1 ), b9] <= [(x `1 ), (x `2 )] by A1, YELLOW_3: 11;

      then

       A3: [(x `1 ), b9] in ( downarrow [(x `1 ), (x `2 )]) by WAYBEL_0: 17;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hence thesis by A3, XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:40

    for S,T be non empty RelStr, s be Element of S, t be Element of T holds [:( uparrow s), ( uparrow t):] = ( uparrow [s, t])

    proof

      let S,T be non empty RelStr, s be Element of S, t be Element of T;

      hereby

        let x be object;

        assume x in [:( uparrow s), ( uparrow t):];

        then

        consider x1,x2 be object such that

         A1: x1 in ( uparrow s) and

         A2: x2 in ( uparrow t) and

         A3: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x2 as Element of T by A2;

        reconsider x1 as Element of S by A1;

        s <= x1 & t <= x2 by A1, A2, WAYBEL_0: 18;

        then [s, t] <= [x1, x2] by YELLOW_3: 11;

        hence x in ( uparrow [s, t]) by A3, WAYBEL_0: 18;

      end;

      let x be object;

      assume

       A4: x in ( uparrow [s, t]);

      then

      reconsider x9 = x as Element of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A5: x9 = [(x9 `1 ), (x9 `2 )] by MCART_1: 21;

      

       A6: [s, t] <= x9 by A4, WAYBEL_0: 18;

      then t <= (x9 `2 ) by A5, YELLOW_3: 11;

      then

       A7: (x `2 ) in ( uparrow t) by WAYBEL_0: 18;

      s <= (x9 `1 ) by A5, A6, YELLOW_3: 11;

      then (x `1 ) in ( uparrow s) by WAYBEL_0: 18;

      hence thesis by A5, A7, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:41

    

     Th41: for S,T be non empty RelStr, x be Element of [:S, T:] holds ( proj1 ( uparrow x)) c= ( uparrow (x `1 )) & ( proj2 ( uparrow x)) c= ( uparrow (x `2 ))

    proof

      let S,T be non empty RelStr, x be Element of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hereby

        let a be object;

        assume a in ( proj1 ( uparrow x));

        then

        consider b be object such that

         A3: [a, b] in ( uparrow x) by XTUPLE_0:def 12;

        reconsider b as Element of T by A1, A3, ZFMISC_1: 87;

        reconsider a9 = a as Element of S by A1, A3, ZFMISC_1: 87;

         [a9, b] >= x by A3, WAYBEL_0: 18;

        then a9 >= (x `1 ) by A2, YELLOW_3: 11;

        hence a in ( uparrow (x `1 )) by WAYBEL_0: 18;

      end;

      let b be object;

      assume b in ( proj2 ( uparrow x));

      then

      consider a be object such that

       A4: [a, b] in ( uparrow x) by XTUPLE_0:def 13;

      reconsider a as Element of S by A1, A4, ZFMISC_1: 87;

      reconsider b9 = b as Element of T by A1, A4, ZFMISC_1: 87;

       [a, b9] >= x by A4, WAYBEL_0: 18;

      then b9 >= (x `2 ) by A2, YELLOW_3: 11;

      hence thesis by WAYBEL_0: 18;

    end;

    theorem :: YELLOW10:42

    for S be non empty RelStr, T be non empty reflexive RelStr, x be Element of [:S, T:] holds ( proj1 ( uparrow x)) = ( uparrow (x `1 ))

    proof

      let S be non empty RelStr, T be non empty reflexive RelStr, x be Element of [:S, T:];

      

       A1: (x `2 ) <= (x `2 );

      thus ( proj1 ( uparrow x)) c= ( uparrow (x `1 )) by Th41;

      let a be object;

      assume

       A2: a in ( uparrow (x `1 ));

      then

      reconsider a9 = a as Element of S;

      a9 >= (x `1 ) by A2, WAYBEL_0: 18;

      then [a9, (x `2 )] >= [(x `1 ), (x `2 )] by A1, YELLOW_3: 11;

      then

       A3: [a9, (x `2 )] in ( uparrow [(x `1 ), (x `2 )]) by WAYBEL_0: 18;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hence thesis by A3, XTUPLE_0:def 12;

    end;

    theorem :: YELLOW10:43

    for S be non empty reflexive RelStr, T be non empty RelStr, x be Element of [:S, T:] holds ( proj2 ( uparrow x)) = ( uparrow (x `2 ))

    proof

      let S be non empty reflexive RelStr, T be non empty RelStr, x be Element of [:S, T:];

      

       A1: (x `1 ) <= (x `1 );

      thus ( proj2 ( uparrow x)) c= ( uparrow (x `2 )) by Th41;

      let b be object;

      assume

       A2: b in ( uparrow (x `2 ));

      then

      reconsider b9 = b as Element of T;

      b9 >= (x `2 ) by A2, WAYBEL_0: 18;

      then [(x `1 ), b9] >= [(x `1 ), (x `2 )] by A1, YELLOW_3: 11;

      then

       A3: [(x `1 ), b9] in ( uparrow [(x `1 ), (x `2 )]) by WAYBEL_0: 18;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hence thesis by A3, XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:44

    

     Th44: for S,T be up-complete non empty Poset, s be Element of S, t be Element of T holds [:( waybelow s), ( waybelow t):] = ( waybelow [s, t])

    proof

      let S,T be up-complete non empty Poset, s be Element of S, t be Element of T;

      hereby

        let x be object;

        assume x in [:( waybelow s), ( waybelow t):];

        then

        consider x1,x2 be object such that

         A1: x1 in ( waybelow s) and

         A2: x2 in ( waybelow t) and

         A3: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x2 as Element of T by A2;

        reconsider x1 as Element of S by A1;

        s >> x1 & t >> x2 by A1, A2, WAYBEL_3: 7;

        then [s, t] >> [x1, x2] by Th19;

        hence x in ( waybelow [s, t]) by A3;

      end;

      let x be object;

      assume

       A4: x in ( waybelow [s, t]);

      then

      reconsider x9 = x as Element of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A5: x9 = [(x9 `1 ), (x9 `2 )] by MCART_1: 21;

      

       A6: [s, t] >> x9 by A4, WAYBEL_3: 7;

      then t >> (x9 `2 ) by A5, Th19;

      then

       A7: (x `2 ) in ( waybelow t);

      s >> (x9 `1 ) by A5, A6, Th19;

      then (x `1 ) in ( waybelow s);

      hence thesis by A5, A7, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:45

    

     Th45: for S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:] holds ( proj1 ( waybelow x)) c= ( waybelow (x `1 )) & ( proj2 ( waybelow x)) c= ( waybelow (x `2 ))

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hereby

        let a be object;

        assume a in ( proj1 ( waybelow x));

        then

        consider b be object such that

         A3: [a, b] in ( waybelow x) by XTUPLE_0:def 12;

        reconsider b as Element of T by A1, A3, ZFMISC_1: 87;

        reconsider a9 = a as Element of S by A1, A3, ZFMISC_1: 87;

         [a9, b] << x by A3, WAYBEL_3: 7;

        then a9 << (x `1 ) by A2, Th18;

        hence a in ( waybelow (x `1 ));

      end;

      let b be object;

      assume b in ( proj2 ( waybelow x));

      then

      consider a be object such that

       A4: [a, b] in ( waybelow x) by XTUPLE_0:def 13;

      reconsider a as Element of S by A1, A4, ZFMISC_1: 87;

      reconsider b9 = b as Element of T by A1, A4, ZFMISC_1: 87;

       [a, b9] << x by A4, WAYBEL_3: 7;

      then b9 << (x `2 ) by A2, Th18;

      hence thesis;

    end;

    theorem :: YELLOW10:46

    

     Th46: for S be up-complete non empty Poset, T be up-complete lower-bounded non empty Poset, x be Element of [:S, T:] holds ( proj1 ( waybelow x)) = ( waybelow (x `1 ))

    proof

      let S be up-complete non empty Poset, T be up-complete lower-bounded non empty Poset, x be Element of [:S, T:];

      

       A1: ( Bottom T) << (x `2 ) by WAYBEL_3: 4;

      thus ( proj1 ( waybelow x)) c= ( waybelow (x `1 )) by Th45;

      let a be object;

      assume

       A2: a in ( waybelow (x `1 ));

      then

      reconsider a9 = a as Element of S;

      a9 << (x `1 ) by A2, WAYBEL_3: 7;

      then [a9, ( Bottom T)] << [(x `1 ), (x `2 )] by A1, Th19;

      then

       A3: [a9, ( Bottom T)] in ( waybelow [(x `1 ), (x `2 )]);

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hence thesis by A3, XTUPLE_0:def 12;

    end;

    theorem :: YELLOW10:47

    

     Th47: for S be up-complete lower-bounded non empty Poset, T be up-complete non empty Poset, x be Element of [:S, T:] holds ( proj2 ( waybelow x)) = ( waybelow (x `2 ))

    proof

      let S be up-complete lower-bounded non empty Poset, T be up-complete non empty Poset, x be Element of [:S, T:];

      

       A1: ( Bottom S) << (x `1 ) by WAYBEL_3: 4;

      thus ( proj2 ( waybelow x)) c= ( waybelow (x `2 )) by Th45;

      let a be object;

      assume

       A2: a in ( waybelow (x `2 ));

      then

      reconsider a9 = a as Element of T;

      a9 << (x `2 ) by A2, WAYBEL_3: 7;

      then [( Bottom S), a9] << [(x `1 ), (x `2 )] by A1, Th19;

      then

       A3: [( Bottom S), a9] in ( waybelow [(x `1 ), (x `2 )]);

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hence thesis by A3, XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:48

    for S,T be up-complete non empty Poset, s be Element of S, t be Element of T holds [:( wayabove s), ( wayabove t):] = ( wayabove [s, t])

    proof

      let S,T be up-complete non empty Poset, s be Element of S, t be Element of T;

      hereby

        let x be object;

        assume x in [:( wayabove s), ( wayabove t):];

        then

        consider x1,x2 be object such that

         A1: x1 in ( wayabove s) and

         A2: x2 in ( wayabove t) and

         A3: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x2 as Element of T by A2;

        reconsider x1 as Element of S by A1;

        s << x1 & t << x2 by A1, A2, WAYBEL_3: 8;

        then [s, t] << [x1, x2] by Th19;

        hence x in ( wayabove [s, t]) by A3;

      end;

      let x be object;

      assume

       A4: x in ( wayabove [s, t]);

      then

      reconsider x9 = x as Element of [:S, T:];

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A5: x9 = [(x9 `1 ), (x9 `2 )] by MCART_1: 21;

      

       A6: [s, t] << x9 by A4, WAYBEL_3: 8;

      then t << (x9 `2 ) by A5, Th19;

      then

       A7: (x `2 ) in ( wayabove t);

      s << (x9 `1 ) by A5, A6, Th19;

      then (x `1 ) in ( wayabove s);

      hence thesis by A5, A7, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:49

    for S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:] holds ( proj1 ( wayabove x)) c= ( wayabove (x `1 )) & ( proj2 ( wayabove x)) c= ( wayabove (x `2 ))

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hereby

        let a be object;

        assume a in ( proj1 ( wayabove x));

        then

        consider b be object such that

         A3: [a, b] in ( wayabove x) by XTUPLE_0:def 12;

        reconsider b as Element of T by A1, A3, ZFMISC_1: 87;

        reconsider a9 = a as Element of S by A1, A3, ZFMISC_1: 87;

         [a9, b] >> x by A3, WAYBEL_3: 8;

        then a9 >> (x `1 ) by A2, Th18;

        hence a in ( wayabove (x `1 ));

      end;

      let b be object;

      assume b in ( proj2 ( wayabove x));

      then

      consider a be object such that

       A4: [a, b] in ( wayabove x) by XTUPLE_0:def 13;

      reconsider a as Element of S by A1, A4, ZFMISC_1: 87;

      reconsider b9 = b as Element of T by A1, A4, ZFMISC_1: 87;

       [a, b9] >> x by A4, WAYBEL_3: 8;

      then b9 >> (x `2 ) by A2, Th18;

      hence thesis;

    end;

    theorem :: YELLOW10:50

    

     Th50: for S,T be up-complete non empty Poset, s be Element of S, t be Element of T holds [:( compactbelow s), ( compactbelow t):] = ( compactbelow [s, t])

    proof

      let S,T be up-complete non empty Poset, s be Element of S, t be Element of T;

      hereby

        let x be object;

        assume x in [:( compactbelow s), ( compactbelow t):];

        then

        consider x1,x2 be object such that

         A1: x1 in ( compactbelow s) and

         A2: x2 in ( compactbelow t) and

         A3: x = [x1, x2] by ZFMISC_1:def 2;

        reconsider x2 as Element of T by A2;

        reconsider x1 as Element of S by A1;

        s >= x1 & t >= x2 by A1, A2, WAYBEL_8: 4;

        then

         A4: [s, t] >= [x1, x2] by YELLOW_3: 11;

        

         A5: ( [x1, x2] `1 ) = x1 & ( [x1, x2] `2 ) = x2;

        x1 is compact & x2 is compact by A1, A2, WAYBEL_8: 4;

        then [x1, x2] is compact by A5, Th23;

        hence x in ( compactbelow [s, t]) by A3, A4;

      end;

      let x be object;

      assume

       A6: x in ( compactbelow [s, t]);

      then

      reconsider x9 = x as Element of [:S, T:];

      

       A7: x9 is compact by A6, WAYBEL_8: 4;

      then

       A8: (x9 `1 ) is compact by Th22;

      

       A9: (x9 `2 ) is compact by A7, Th22;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A10: x9 = [(x9 `1 ), (x9 `2 )] by MCART_1: 21;

      

       A11: [s, t] >= x9 by A6, WAYBEL_8: 4;

      then t >= (x9 `2 ) by A10, YELLOW_3: 11;

      then

       A12: (x `2 ) in ( compactbelow t) by A9;

      s >= (x9 `1 ) by A10, A11, YELLOW_3: 11;

      then (x `1 ) in ( compactbelow s) by A8;

      hence thesis by A10, A12, ZFMISC_1:def 2;

    end;

    theorem :: YELLOW10:51

    

     Th51: for S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:] holds ( proj1 ( compactbelow x)) c= ( compactbelow (x `1 )) & ( proj2 ( compactbelow x)) c= ( compactbelow (x `2 ))

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, x be Element of [:S, T:];

      

       A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A2: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      hereby

        let a be object;

        assume a in ( proj1 ( compactbelow x));

        then

        consider b be object such that

         A3: [a, b] in ( compactbelow x) by XTUPLE_0:def 12;

        reconsider b as Element of T by A1, A3, ZFMISC_1: 87;

        reconsider a9 = a as Element of S by A1, A3, ZFMISC_1: 87;

        ( [a9, b] `1 ) = a9 & [a9, b] is compact by A3, WAYBEL_8: 4;

        then

         A4: a9 is compact by Th22;

         [a9, b] <= x by A3, WAYBEL_8: 4;

        then a9 <= (x `1 ) by A2, YELLOW_3: 11;

        hence a in ( compactbelow (x `1 )) by A4;

      end;

      let b be object;

      assume b in ( proj2 ( compactbelow x));

      then

      consider a be object such that

       A5: [a, b] in ( compactbelow x) by XTUPLE_0:def 13;

      reconsider a as Element of S by A1, A5, ZFMISC_1: 87;

      reconsider b9 = b as Element of T by A1, A5, ZFMISC_1: 87;

      ( [a, b9] `2 ) = b9 & [a, b9] is compact by A5, WAYBEL_8: 4;

      then

       A6: b9 is compact by Th22;

       [a, b9] <= x by A5, WAYBEL_8: 4;

      then b9 <= (x `2 ) by A2, YELLOW_3: 11;

      hence thesis by A6;

    end;

    theorem :: YELLOW10:52

    

     Th52: for S be up-complete non empty Poset, T be up-complete lower-bounded non empty Poset, x be Element of [:S, T:] holds ( proj1 ( compactbelow x)) = ( compactbelow (x `1 ))

    proof

      let S be up-complete non empty Poset, T be up-complete lower-bounded non empty Poset, x be Element of [:S, T:];

      

       A1: ( Bottom T) <= (x `2 ) by YELLOW_0: 44;

      thus ( proj1 ( compactbelow x)) c= ( compactbelow (x `1 )) by Th51;

      let a be object;

      assume

       A2: a in ( compactbelow (x `1 ));

      then

      reconsider a9 = a as Element of S;

      a9 <= (x `1 ) by A2, WAYBEL_8: 4;

      then

       A3: [a9, ( Bottom T)] <= [(x `1 ), (x `2 )] by A1, YELLOW_3: 11;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A4: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      

       A5: ( [a9, ( Bottom T)] `1 ) = a9 & ( [a9, ( Bottom T)] `2 ) = ( Bottom T);

      a9 is compact by A2, WAYBEL_8: 4;

      then [a9, ( Bottom T)] is compact by A5, Th23, WAYBEL_3: 15;

      then [a9, ( Bottom T)] in ( compactbelow [(x `1 ), (x `2 )]) by A3;

      hence thesis by A4, XTUPLE_0:def 12;

    end;

    theorem :: YELLOW10:53

    

     Th53: for S be up-complete lower-bounded non empty Poset, T be up-complete non empty Poset, x be Element of [:S, T:] holds ( proj2 ( compactbelow x)) = ( compactbelow (x `2 ))

    proof

      let S be up-complete lower-bounded non empty Poset, T be up-complete non empty Poset, x be Element of [:S, T:];

      

       A1: ( Bottom S) <= (x `1 ) by YELLOW_0: 44;

      thus ( proj2 ( compactbelow x)) c= ( compactbelow (x `2 )) by Th51;

      let a be object;

      assume

       A2: a in ( compactbelow (x `2 ));

      then

      reconsider a9 = a as Element of T;

      a9 <= (x `2 ) by A2, WAYBEL_8: 4;

      then

       A3: [( Bottom S), a9] <= [(x `1 ), (x `2 )] by A1, YELLOW_3: 11;

      the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

       A4: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      

       A5: ( [( Bottom S), a9] `1 ) = ( Bottom S) & ( [( Bottom S), a9] `2 ) = a9;

      a9 is compact by A2, WAYBEL_8: 4;

      then [( Bottom S), a9] is compact by A5, Th23, WAYBEL_3: 15;

      then [( Bottom S), a9] in ( compactbelow [(x `1 ), (x `2 )]) by A3;

      hence thesis by A4, XTUPLE_0:def 13;

    end;

    registration

      let S be non empty reflexive RelStr;

      cluster empty -> Open for Subset of S;

      coherence

      proof

        let X be Subset of S such that

         A1: X is empty;

        let x be Element of S;

        assume x in X;

        hence thesis by A1;

      end;

    end

    theorem :: YELLOW10:54

    for S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of [:S, T:] st X is Open holds ( proj1 X) is Open & ( proj2 X) is Open

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of [:S, T:] such that

       A1: for x be Element of [:S, T:] st x in X holds ex y be Element of [:S, T:] st y in X & y << x;

      

       A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      hereby

        let s be Element of S;

        assume s in ( proj1 X);

        then

        consider t be object such that

         A3: [s, t] in X by XTUPLE_0:def 12;

        reconsider t as Element of T by A2, A3, ZFMISC_1: 87;

        consider y be Element of [:S, T:] such that

         A4: y in X and

         A5: y << [s, t] by A1, A3;

        take z = (y `1 );

        

         A6: y = [(y `1 ), (y `2 )] by A2, MCART_1: 21;

        hence z in ( proj1 X) by A4, XTUPLE_0:def 12;

        thus z << s by A5, A6, Th18;

      end;

      let t be Element of T;

      assume t in ( proj2 X);

      then

      consider s be object such that

       A7: [s, t] in X by XTUPLE_0:def 13;

      reconsider s as Element of S by A2, A7, ZFMISC_1: 87;

      consider y be Element of [:S, T:] such that

       A8: y in X and

       A9: y << [s, t] by A1, A7;

      take z = (y `2 );

      

       A10: y = [(y `1 ), (y `2 )] by A2, MCART_1: 21;

      hence z in ( proj2 X) by A8, XTUPLE_0:def 13;

      thus thesis by A9, A10, Th18;

    end;

    theorem :: YELLOW10:55

    for S,T be up-complete non empty Poset, X be Subset of S, Y be Subset of T st X is Open & Y is Open holds [:X, Y:] is Open

    proof

      let S,T be up-complete non empty Poset, X be Subset of S, Y be Subset of T such that

       A1: for x be Element of S st x in X holds ex y be Element of S st y in X & y << x and

       A2: for x be Element of T st x in Y holds ex y be Element of T st y in Y & y << x;

      let x be Element of [:S, T:];

      assume

       A3: x in [:X, Y:];

      then

       A4: x = [(x `1 ), (x `2 )] by MCART_1: 21;

      then (x `1 ) in X by A3, ZFMISC_1: 87;

      then

      consider s be Element of S such that

       A5: s in X and

       A6: s << (x `1 ) by A1;

      (x `2 ) in Y by A3, A4, ZFMISC_1: 87;

      then

      consider t be Element of T such that

       A7: t in Y and

       A8: t << (x `2 ) by A2;

      reconsider t as Element of T;

      take [s, t];

      thus [s, t] in [:X, Y:] by A5, A7, ZFMISC_1: 87;

      thus thesis by A4, A6, A8, Th19;

    end;

    theorem :: YELLOW10:56

    for S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of [:S, T:] st X is inaccessible holds ( proj1 X) is inaccessible & ( proj2 X) is inaccessible

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of [:S, T:] such that

       A1: for D be non empty directed Subset of [:S, T:] st ( sup D) in X holds D meets X;

      

       A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      hereby

        let D be non empty directed Subset of S;

        assume ( sup D) in ( proj1 X);

        then

        consider t be object such that

         A3: [( sup D), t] in X by XTUPLE_0:def 12;

        

         A4: t in the carrier of T by A2, A3, ZFMISC_1: 87;

        then

        reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0: 5;

         ex_sup_of ( [:D, t9:], [:S, T:]) by WAYBEL_0: 75;

        

        then ( sup [:D, t9:]) = [( sup ( proj1 [:D, t9:])), ( sup ( proj2 [:D, t9:]))] by YELLOW_3: 46

        .= [( sup D), ( sup ( proj2 [:D, t9:]))] by FUNCT_5: 9

        .= [( sup D), ( sup t9)] by FUNCT_5: 9

        .= [( sup D), t] by A4, YELLOW_0: 39;

        then [:D, {t}:] meets X by A1, A3;

        then

        consider x be object such that

         A5: x in [:D, {t}:] and

         A6: x in X by XBOOLE_0: 3;

        now

          take a = (x `1 );

          x = [a, (x `2 )] by A5, MCART_1: 21;

          hence a in D & a in ( proj1 X) by A5, A6, XTUPLE_0:def 12, ZFMISC_1: 87;

        end;

        hence D meets ( proj1 X) by XBOOLE_0: 3;

      end;

      let D be non empty directed Subset of T;

      assume ( sup D) in ( proj2 X);

      then

      consider s be object such that

       A7: [s, ( sup D)] in X by XTUPLE_0:def 13;

      

       A8: s in the carrier of S by A2, A7, ZFMISC_1: 87;

      then

      reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0: 5;

       ex_sup_of ( [:s9, D:], [:S, T:]) by WAYBEL_0: 75;

      

      then ( sup [:s9, D:]) = [( sup ( proj1 [:s9, D:])), ( sup ( proj2 [:s9, D:]))] by YELLOW_3: 46

      .= [( sup s9), ( sup ( proj2 [:s9, D:]))] by FUNCT_5: 9

      .= [( sup s9), ( sup D)] by FUNCT_5: 9

      .= [s, ( sup D)] by A8, YELLOW_0: 39;

      then [: {s}, D:] meets X by A1, A7;

      then

      consider x be object such that

       A9: x in [: {s}, D:] and

       A10: x in X by XBOOLE_0: 3;

      now

        take a = (x `2 );

        x = [(x `1 ), a] by A9, MCART_1: 21;

        hence a in D & a in ( proj2 X) by A9, A10, XTUPLE_0:def 13, ZFMISC_1: 87;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: YELLOW10:57

    for S,T be antisymmetric up-complete non empty reflexive RelStr, X be upper Subset of S, Y be upper Subset of T st X is inaccessible & Y is inaccessible holds [:X, Y:] is inaccessible

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, X be upper Subset of S, Y be upper Subset of T such that

       A1: for D be non empty directed Subset of S st ( sup D) in X holds D meets X and

       A2: for D be non empty directed Subset of T st ( sup D) in Y holds D meets Y;

      let D be non empty directed Subset of [:S, T:] such that

       A3: ( sup D) in [:X, Y:];

       ex_sup_of (D, [:S, T:]) by WAYBEL_0: 75;

      then

       A4: ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))] by YELLOW_3: 46;

      then ( proj1 D) is non empty directed & ( sup ( proj1 D)) in X by A3, YELLOW_3: 21, YELLOW_3: 22, ZFMISC_1: 87;

      then ( proj1 D) meets X by A1;

      then

      consider s be object such that

       A5: s in ( proj1 D) and

       A6: s in X by XBOOLE_0: 3;

      reconsider s as Element of S by A5;

      consider s2 be object such that

       A7: [s, s2] in D by A5, XTUPLE_0:def 12;

      ( proj2 D) is non empty directed & ( sup ( proj2 D)) in Y by A3, A4, YELLOW_3: 21, YELLOW_3: 22, ZFMISC_1: 87;

      then ( proj2 D) meets Y by A2;

      then

      consider t be object such that

       A8: t in ( proj2 D) and

       A9: t in Y by XBOOLE_0: 3;

      reconsider t as Element of T by A8;

      consider t1 be object such that

       A10: [t1, t] in D by A8, XTUPLE_0:def 13;

      

       A11: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider s2 as Element of T by A7, ZFMISC_1: 87;

      reconsider t1 as Element of S by A11, A10, ZFMISC_1: 87;

      consider z be Element of [:S, T:] such that

       A12: z in D and

       A13: [s, s2] <= z and

       A14: [t1, t] <= z by A7, A10, WAYBEL_0:def 1;

      now

        take z;

        thus z in D by A12;

        

         A15: z = [(z `1 ), (z `2 )] by A11, MCART_1: 21;

        then t <= (z `2 ) by A14, YELLOW_3: 11;

        then

         A16: (z `2 ) in Y by A9, WAYBEL_0:def 20;

        s <= (z `1 ) by A13, A15, YELLOW_3: 11;

        then (z `1 ) in X by A6, WAYBEL_0:def 20;

        hence z in [:X, Y:] by A15, A16, ZFMISC_1: 87;

      end;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: YELLOW10:58

    for S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of S, Y be Subset of T st [:X, Y:] is directly_closed holds (Y <> {} implies X is directly_closed) & (X <> {} implies Y is directly_closed)

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of S, Y be Subset of T such that

       A1: for D be non empty directed Subset of [:S, T:] st D c= [:X, Y:] holds ( sup D) in [:X, Y:];

      hereby

        assume

         A2: Y <> {} ;

        thus X is directly_closed

        proof

          consider t be object such that

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

          reconsider t9 = {t} as non empty directed Subset of T by A3, WAYBEL_0: 5;

          

           A4: t9 c= Y by A3, ZFMISC_1: 31;

          let D be non empty directed Subset of S;

          assume D c= X;

          then

           A5: ( sup [:D, t9:]) in [:X, Y:] by A1, A4, ZFMISC_1: 96;

           ex_sup_of ( [:D, t9:], [:S, T:]) by WAYBEL_0: 75;

          

          then ( sup [:D, t9:]) = [( sup ( proj1 [:D, t9:])), ( sup ( proj2 [:D, t9:]))] by YELLOW_3: 46

          .= [( sup D), ( sup ( proj2 [:D, t9:]))] by FUNCT_5: 9

          .= [( sup D), ( sup t9)] by FUNCT_5: 9

          .= [( sup D), t] by A3, YELLOW_0: 39;

          hence thesis by A5, ZFMISC_1: 87;

        end;

      end;

      assume X <> {} ;

      then

      consider s be object such that

       A6: s in X by XBOOLE_0:def 1;

      reconsider s9 = {s} as non empty directed Subset of S by A6, WAYBEL_0: 5;

      let D be non empty directed Subset of T such that

       A7: D c= Y;

       ex_sup_of ( [:s9, D:], [:S, T:]) by WAYBEL_0: 75;

      

      then

       A8: ( sup [:s9, D:]) = [( sup ( proj1 [:s9, D:])), ( sup ( proj2 [:s9, D:]))] by YELLOW_3: 46

      .= [( sup s9), ( sup ( proj2 [:s9, D:]))] by FUNCT_5: 9

      .= [( sup s9), ( sup D)] by FUNCT_5: 9

      .= [s, ( sup D)] by A6, YELLOW_0: 39;

      s9 c= X by A6, ZFMISC_1: 31;

      then ( sup [:s9, D:]) in [:X, Y:] by A1, A7, ZFMISC_1: 96;

      hence thesis by A8, ZFMISC_1: 87;

    end;

    theorem :: YELLOW10:59

    for S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of S, Y be Subset of T st X is directly_closed & Y is directly_closed holds [:X, Y:] is directly_closed

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of S, Y be Subset of T such that

       A1: for D be non empty directed Subset of S st D c= X holds ( sup D) in X and

       A2: for D be non empty directed Subset of T st D c= Y holds ( sup D) in Y;

      let D be non empty directed Subset of [:S, T:];

      assume

       A3: D c= [:X, Y:];

      ( proj2 D) is non empty directed by YELLOW_3: 21, YELLOW_3: 22;

      then

       A4: ( sup ( proj2 D)) in Y by A2, A3, FUNCT_5: 11;

       ex_sup_of (D, [:S, T:]) by WAYBEL_0: 75;

      then

       A5: ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))] by YELLOW_3: 46;

      ( proj1 D) is non empty directed by YELLOW_3: 21, YELLOW_3: 22;

      then ( sup ( proj1 D)) in X by A1, A3, FUNCT_5: 11;

      hence thesis by A4, A5, ZFMISC_1: 87;

    end;

    theorem :: YELLOW10:60

    for S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of [:S, T:] st X is property(S) holds ( proj1 X) is property(S) & ( proj2 X) is property(S)

    proof

      let S,T be antisymmetric up-complete non empty reflexive RelStr, X be Subset of [:S, T:] such that

       A1: for D be non empty directed Subset of [:S, T:] st ( sup D) in X holds ex y be Element of [:S, T:] st y in D & for x be Element of [:S, T:] st x in D & x >= y holds x in X;

      

       A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      hereby

        let D be non empty directed Subset of S;

        assume ( sup D) in ( proj1 X);

        then

        consider t be object such that

         A3: [( sup D), t] in X by XTUPLE_0:def 12;

        reconsider t as Element of T by A2, A3, ZFMISC_1: 87;

        reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0: 5;

         ex_sup_of ( [:D, t9:], [:S, T:]) by WAYBEL_0: 75;

        

        then ( sup [:D, t9:]) = [( sup ( proj1 [:D, t9:])), ( sup ( proj2 [:D, t9:]))] by YELLOW_3: 46

        .= [( sup D), ( sup ( proj2 [:D, t9:]))] by FUNCT_5: 9

        .= [( sup D), ( sup t9)] by FUNCT_5: 9

        .= [( sup D), t] by YELLOW_0: 39;

        then

        consider y be Element of [:S, T:] such that

         A4: y in [:D, t9:] and

         A5: for x be Element of [:S, T:] st x in [:D, t9:] & x >= y holds x in X by A1, A3;

        take z = (y `1 );

        

         A6: y = [(y `1 ), (y `2 )] by A2, MCART_1: 21;

        hence z in D by A4, ZFMISC_1: 87;

        

         A7: (y `2 ) = t by A4, A6, ZFMISC_1: 106;

        let x be Element of S;

        assume x in D;

        then

         A8: [x, t] in [:D, t9:] by ZFMISC_1: 106;

        

         A9: (y `2 ) <= (y `2 );

        assume x >= z;

        then [x, t] >= y by A6, A7, A9, YELLOW_3: 11;

        then [x, t] in X by A5, A8;

        hence x in ( proj1 X) by XTUPLE_0:def 12;

      end;

      let D be non empty directed Subset of T;

      assume ( sup D) in ( proj2 X);

      then

      consider s be object such that

       A10: [s, ( sup D)] in X by XTUPLE_0:def 13;

      reconsider s as Element of S by A2, A10, ZFMISC_1: 87;

      reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0: 5;

       ex_sup_of ( [:s9, D:], [:S, T:]) by WAYBEL_0: 75;

      

      then ( sup [:s9, D:]) = [( sup ( proj1 [:s9, D:])), ( sup ( proj2 [:s9, D:]))] by YELLOW_3: 46

      .= [( sup s9), ( sup ( proj2 [:s9, D:]))] by FUNCT_5: 9

      .= [( sup s9), ( sup D)] by FUNCT_5: 9

      .= [s, ( sup D)] by YELLOW_0: 39;

      then

      consider y be Element of [:S, T:] such that

       A11: y in [:s9, D:] and

       A12: for x be Element of [:S, T:] st x in [:s9, D:] & x >= y holds x in X by A1, A10;

      take z = (y `2 );

      

       A13: y = [(y `1 ), (y `2 )] by A2, MCART_1: 21;

      hence z in D by A11, ZFMISC_1: 87;

      

       A14: (y `1 ) = s by A11, A13, ZFMISC_1: 105;

      let x be Element of T;

      assume x in D;

      then

       A15: [s, x] in [:s9, D:] by ZFMISC_1: 105;

      

       A16: (y `1 ) <= (y `1 );

      assume x >= z;

      then [s, x] >= y by A13, A14, A16, YELLOW_3: 11;

      then [s, x] in X by A12, A15;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: YELLOW10:61

    for S,T be up-complete non empty Poset, X be Subset of S, Y be Subset of T st X is property(S) & Y is property(S) holds [:X, Y:] is property(S)

    proof

      let S,T be up-complete non empty Poset, X be Subset of S, Y be Subset of T such that

       A1: for D be non empty directed Subset of S st ( sup D) in X holds ex y be Element of S st y in D & for x be Element of S st x in D & x >= y holds x in X and

       A2: for D be non empty directed Subset of T st ( sup D) in Y holds ex y be Element of T st y in D & for x be Element of T st x in D & x >= y holds x in Y;

      let D be non empty directed Subset of [:S, T:] such that

       A3: ( sup D) in [:X, Y:];

       ex_sup_of (D, [:S, T:]) by WAYBEL_0: 75;

      then

       A4: ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))] by YELLOW_3: 46;

      then ( proj1 D) is non empty directed & ( sup ( proj1 D)) in X by A3, YELLOW_3: 21, YELLOW_3: 22, ZFMISC_1: 87;

      then

      consider s be Element of S such that

       A5: s in ( proj1 D) and

       A6: for x be Element of S st x in ( proj1 D) & x >= s holds x in X by A1;

      consider s2 be object such that

       A7: [s, s2] in D by A5, XTUPLE_0:def 12;

      ( proj2 D) is non empty directed & ( sup ( proj2 D)) in Y by A3, A4, YELLOW_3: 21, YELLOW_3: 22, ZFMISC_1: 87;

      then

      consider t be Element of T such that

       A8: t in ( proj2 D) and

       A9: for x be Element of T st x in ( proj2 D) & x >= t holds x in Y by A2;

      consider t1 be object such that

       A10: [t1, t] in D by A8, XTUPLE_0:def 13;

      

       A11: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider s2 as Element of T by A7, ZFMISC_1: 87;

      reconsider t1 as Element of S by A11, A10, ZFMISC_1: 87;

      consider z be Element of [:S, T:] such that

       A12: z in D and

       A13: [s, s2] <= z and

       A14: [t1, t] <= z by A7, A10, WAYBEL_0:def 1;

      

       A15: z = [(z `1 ), (z `2 )] by A11, MCART_1: 21;

      then

       A16: t <= (z `2 ) by A14, YELLOW_3: 11;

      take z;

      thus z in D by A12;

      let x be Element of [:S, T:] such that

       A17: x in D;

      assume

       A18: x >= z;

      then

       A19: (x `2 ) >= (z `2 ) by YELLOW_3: 12;

      

       A20: x = [(x `1 ), (x `2 )] by A11, MCART_1: 21;

      then (x `2 ) in ( proj2 D) by A17, XTUPLE_0:def 13;

      then

       A21: (x `2 ) in Y by A9, A19, A16, ORDERS_2: 3;

      

       A22: s <= (z `1 ) by A13, A15, YELLOW_3: 11;

      

       A23: (x `1 ) >= (z `1 ) by A18, YELLOW_3: 12;

      (x `1 ) in ( proj1 D) by A17, A20, XTUPLE_0:def 12;

      then (x `1 ) in X by A6, A23, A22, ORDERS_2: 3;

      hence thesis by A20, A21, ZFMISC_1: 87;

    end;

    begin

    theorem :: YELLOW10:62

    

     Th62: for S,T be non empty reflexive RelStr st the RelStr of S = the RelStr of T & S is /\-complete holds T is /\-complete

    proof

      let S,T be non empty reflexive RelStr such that

       A1: the RelStr of S = the RelStr of T and

       A2: for X be non empty Subset of S holds ex x be Element of S st x is_<=_than X & for y be Element of S st y is_<=_than X holds x >= y;

      let X be non empty Subset of T;

      consider x be Element of S such that

       A3: x is_<=_than X and

       A4: for y be Element of S st y is_<=_than X holds x >= y by A1, A2;

      reconsider z = x as Element of T by A1;

      take z;

      thus z is_<=_than X by A1, A3, YELLOW_0: 2;

      let y be Element of T;

      reconsider s = y as Element of S by A1;

      assume y is_<=_than X;

      then x >= s by A1, A4, YELLOW_0: 2;

      hence thesis by A1, YELLOW_0: 1;

    end;

    registration

      let S be /\-complete non empty reflexive RelStr;

      cluster the RelStr of S -> /\-complete;

      coherence by Th62;

    end

    registration

      let S,T be /\-complete non empty reflexive RelStr;

      cluster [:S, T:] -> /\-complete;

      coherence

      proof

        let X be non empty Subset of [:S, T:];

        ( proj1 X) is non empty by YELLOW_3: 21;

        then

        consider s be Element of S such that

         A1: s is_<=_than ( proj1 X) and

         A2: for y be Element of S st y is_<=_than ( proj1 X) holds s >= y by WAYBEL_0:def 40;

        ( proj2 X) is non empty by YELLOW_3: 21;

        then

        consider t be Element of T such that

         A3: t is_<=_than ( proj2 X) and

         A4: for y be Element of T st y is_<=_than ( proj2 X) holds t >= y by WAYBEL_0:def 40;

        take [s, t];

        thus [s, t] is_<=_than X by A1, A3, YELLOW_3: 34;

        let y be Element of [:S, T:];

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

         A5: y = [(y `1 ), (y `2 )] by MCART_1: 21;

        assume

         A6: y is_<=_than X;

        then (y `2 ) is_<=_than ( proj2 X) by A5, YELLOW_3: 34;

        then

         A7: t >= (y `2 ) by A4;

        (y `1 ) is_<=_than ( proj1 X) by A5, A6, YELLOW_3: 34;

        then s >= (y `1 ) by A2;

        hence thesis by A5, A7, YELLOW_3: 11;

      end;

    end

    theorem :: YELLOW10:63

    for S,T be non empty reflexive RelStr st [:S, T:] is /\-complete holds S is /\-complete & T is /\-complete

    proof

      let S,T be non empty reflexive RelStr such that

       A1: for X be non empty Subset of [:S, T:] holds ex x be Element of [:S, T:] st x is_<=_than X & for y be Element of [:S, T:] st y is_<=_than X holds x >= y;

      

       A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

      thus S is /\-complete

      proof

        set t = the Element of T;

        let X be non empty Subset of S;

        consider x be Element of [:S, T:] such that

         A3: x is_<=_than [:X, {t}:] and

         A4: for y be Element of [:S, T:] st y is_<=_than [:X, {t}:] holds x >= y by A1;

        take (x `1 );

        

         A5: x = [(x `1 ), (x `2 )] by A2, MCART_1: 21;

        hence (x `1 ) is_<=_than X by A3, YELLOW_3: 32;

        t <= t;

        then

         A6: t is_<=_than {t} by YELLOW_0: 7;

        let y be Element of S;

        assume y is_<=_than X;

        then x >= [y, t] by A4, A6, YELLOW_3: 33;

        hence thesis by A5, YELLOW_3: 11;

      end;

      set s = the Element of S;

      let X be non empty Subset of T;

      consider x be Element of [:S, T:] such that

       A7: x is_<=_than [: {s}, X:] and

       A8: for y be Element of [:S, T:] st y is_<=_than [: {s}, X:] holds x >= y by A1;

      take (x `2 );

      

       A9: x = [(x `1 ), (x `2 )] by A2, MCART_1: 21;

      hence (x `2 ) is_<=_than X by A7, YELLOW_3: 32;

      s <= s;

      then

       A10: s is_<=_than {s} by YELLOW_0: 7;

      let y be Element of T;

      assume y is_<=_than X;

      then x >= [s, y] by A8, A10, YELLOW_3: 33;

      hence thesis by A9, YELLOW_3: 11;

    end;

    registration

      let S,T be complemented bounded with_infima with_suprema antisymmetric non empty RelStr;

      cluster [:S, T:] -> complemented;

      coherence

      proof

        let x be Element of [:S, T:];

        consider s be Element of S such that

         A1: s is_a_complement_of (x `1 ) by WAYBEL_1:def 24;

        consider t be Element of T such that

         A2: t is_a_complement_of (x `2 ) by WAYBEL_1:def 24;

        take [s, t];

        ( [s, t] `1 ) = s & ( [s, t] `2 ) = t;

        hence [s, t] is_a_complement_of x by A1, A2, Th17;

      end;

    end

    theorem :: YELLOW10:64

    for S,T be bounded with_infima with_suprema antisymmetric RelStr st [:S, T:] is complemented holds S is complemented & T is complemented

    proof

      let S,T be bounded with_infima with_suprema antisymmetric RelStr;

      set s = the Element of S;

      assume

       A1: for x be Element of [:S, T:] holds ex y be Element of [:S, T:] st y is_a_complement_of x;

      thus S is complemented

      proof

        set t = the Element of T;

        let s be Element of S;

        consider y be Element of [:S, T:] such that

         A2: y is_a_complement_of [s, t] by A1;

        take (y `1 );

        ( [s, t] `1 ) = s;

        hence (y `1 ) is_a_complement_of s by A2, Th17;

      end;

      let t be Element of T;

      consider y be Element of [:S, T:] such that

       A3: y is_a_complement_of [s, t] by A1;

      take (y `2 );

      ( [s, t] `2 ) = t;

      hence (y `2 ) is_a_complement_of t by A3, Th17;

    end;

    registration

      let S,T be distributive with_infima with_suprema antisymmetric non empty RelStr;

      cluster [:S, T:] -> distributive;

      coherence

      proof

        let x,y,z be Element of [:S, T:];

        

         A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        

         A2: ((x "/\" (y "\/" z)) `2 ) = ((x `2 ) "/\" ((y "\/" z) `2 )) by Th13

        .= ((x `2 ) "/\" ((y `2 ) "\/" (z `2 ))) by Th14

        .= (((x `2 ) "/\" (y `2 )) "\/" ((x `2 ) "/\" (z `2 ))) by WAYBEL_1:def 3

        .= (((x "/\" y) `2 ) "\/" ((x `2 ) "/\" (z `2 ))) by Th13

        .= (((x "/\" y) `2 ) "\/" ((x "/\" z) `2 )) by Th13

        .= (((x "/\" y) "\/" (x "/\" z)) `2 ) by Th14;

        ((x "/\" (y "\/" z)) `1 ) = ((x `1 ) "/\" ((y "\/" z) `1 )) by Th13

        .= ((x `1 ) "/\" ((y `1 ) "\/" (z `1 ))) by Th14

        .= (((x `1 ) "/\" (y `1 )) "\/" ((x `1 ) "/\" (z `1 ))) by WAYBEL_1:def 3

        .= (((x "/\" y) `1 ) "\/" ((x `1 ) "/\" (z `1 ))) by Th13

        .= (((x "/\" y) `1 ) "\/" ((x "/\" z) `1 )) by Th13

        .= (((x "/\" y) "\/" (x "/\" z)) `1 ) by Th14;

        hence (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z)) by A1, A2, DOMAIN_1: 2;

      end;

    end

    theorem :: YELLOW10:65

    for S be with_infima with_suprema antisymmetric RelStr, T be with_infima with_suprema reflexive antisymmetric RelStr st [:S, T:] is distributive holds S is distributive

    proof

      let S be with_infima with_suprema antisymmetric RelStr, T be with_infima with_suprema reflexive antisymmetric RelStr such that

       A1: for x,y,z be Element of [:S, T:] holds (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z));

      set t = the Element of T;

      let x,y,z be Element of S;

      

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

      t <= t;

      then

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

      

      thus (x "/\" (y "\/" z)) = ( [(x "/\" (y "\/" z)), t] `1 )

      .= (( [x, t] "/\" [(y "\/" z), t]) `1 ) by A2, Th15

      .= (( [x, t] "/\" ( [y, t] "\/" [z, t])) `1 ) by A3, Th16

      .= ((( [x, t] "/\" [y, t]) "\/" ( [x, t] "/\" [z, t])) `1 ) by A1

      .= (( [(x "/\" y), t] "\/" ( [x, t] "/\" [z, t])) `1 ) by A2, Th15

      .= (( [(x "/\" y), t] "\/" [(x "/\" z), t]) `1 ) by A2, Th15

      .= ( [((x "/\" y) "\/" (x "/\" z)), t] `1 ) by A3, Th16

      .= ((x "/\" y) "\/" (x "/\" z));

    end;

    theorem :: YELLOW10:66

    for S be with_infima with_suprema reflexive antisymmetric RelStr, T be with_infima with_suprema antisymmetric RelStr st [:S, T:] is distributive holds T is distributive

    proof

      let S be with_infima with_suprema reflexive antisymmetric RelStr, T be with_infima with_suprema antisymmetric RelStr such that

       A1: for x,y,z be Element of [:S, T:] holds (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z));

      set s = the Element of S;

      let x,y,z be Element of T;

      

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

      s <= s;

      then

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

      

      thus (x "/\" (y "\/" z)) = ( [s, (x "/\" (y "\/" z))] `2 )

      .= (( [s, x] "/\" [s, (y "\/" z)]) `2 ) by A2, Th15

      .= (( [s, x] "/\" ( [s, y] "\/" [s, z])) `2 ) by A3, Th16

      .= ((( [s, x] "/\" [s, y]) "\/" ( [s, x] "/\" [s, z])) `2 ) by A1

      .= (( [s, (x "/\" y)] "\/" ( [s, x] "/\" [s, z])) `2 ) by A2, Th15

      .= (( [s, (x "/\" y)] "\/" [s, (x "/\" z)]) `2 ) by A2, Th15

      .= ( [s, ((x "/\" y) "\/" (x "/\" z))] `2 ) by A3, Th16

      .= ((x "/\" y) "\/" (x "/\" z));

    end;

    registration

      let S,T be meet-continuous Semilattice;

      cluster [:S, T:] -> satisfying_MC;

      coherence

      proof

        let x be Element of [:S, T:], D be non empty directed Subset of [:S, T:];

        

         A1: ( proj1 D) is non empty directed by YELLOW_3: 21, YELLOW_3: 22;

        reconsider x9 = {x} as non empty directed Subset of [:S, T:] by WAYBEL_0: 5;

        

         A2: ( proj2 D) is non empty directed by YELLOW_3: 21, YELLOW_3: 22;

        

         A3: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        then

         A4: x = [(x `1 ), (x `2 )] by MCART_1: 21;

         ex_sup_of ((x9 "/\" D), [:S, T:]) by WAYBEL_0: 75;

        then

         A5: ( sup ( {x} "/\" D)) = [( sup ( proj1 ( {x} "/\" D))), ( sup ( proj2 ( {x} "/\" D)))] by YELLOW_3: 46;

         ex_sup_of (D, [:S, T:]) by WAYBEL_0: 75;

        then

         A6: ( sup D) = [( sup ( proj1 D)), ( sup ( proj2 D))] by YELLOW_3: 46;

        

         A7: ((x "/\" ( sup D)) `2 ) = ((x `2 ) "/\" (( sup D) `2 )) by Th13

        .= ((x `2 ) "/\" ( sup ( proj2 D))) by A6

        .= ( sup ( {(x `2 )} "/\" ( proj2 D))) by A2, WAYBEL_2:def 6

        .= ( sup (( proj2 {x}) "/\" ( proj2 D))) by A4, FUNCT_5: 12

        .= ( sup ( proj2 ( {x} "/\" D))) by Th24

        .= (( sup ( {x} "/\" D)) `2 ) by A5;

        ((x "/\" ( sup D)) `1 ) = ((x `1 ) "/\" (( sup D) `1 )) by Th13

        .= ((x `1 ) "/\" ( sup ( proj1 D))) by A6

        .= ( sup ( {(x `1 )} "/\" ( proj1 D))) by A1, WAYBEL_2:def 6

        .= ( sup (( proj1 {x}) "/\" ( proj1 D))) by A4, FUNCT_5: 12

        .= ( sup ( proj1 ( {x} "/\" D))) by Th24

        .= (( sup ( {x} "/\" D)) `1 ) by A5;

        hence (x "/\" ( sup D)) = ( sup ( {x} "/\" D)) by A3, A7, DOMAIN_1: 2;

      end;

    end

    theorem :: YELLOW10:67

    for S,T be Semilattice st [:S, T:] is meet-continuous holds S is meet-continuous & T is meet-continuous

    proof

      let S,T be Semilattice such that

       A1: [:S, T:] is up-complete and

       A2: for x be Element of [:S, T:], D be non empty directed Subset of [:S, T:] holds (x "/\" ( sup D)) = ( sup ( {x} "/\" D));

      hereby

        thus S is up-complete by A1, WAYBEL_2: 11;

        set t = the Element of T;

        let s be Element of S, D be non empty directed Subset of S;

        reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0: 5;

        reconsider ST = { [s, t]} as non empty directed Subset of [:S, T:] by WAYBEL_0: 5;

         ex_sup_of ( [:D, t9:], [:S, T:]) by A1, WAYBEL_0: 75;

        then

         A3: ( sup [:D, t9:]) = [( sup ( proj1 [:D, t9:])), ( sup ( proj2 [:D, t9:]))] by YELLOW_3: 46;

         ex_sup_of ((ST "/\" [:D, t9:]), [:S, T:]) by A1, WAYBEL_0: 75;

        then

         A4: ( sup ( { [s, t]} "/\" [:D, t9:])) = [( sup ( proj1 ( { [s, t]} "/\" [:D, t9:]))), ( sup ( proj2 ( { [s, t]} "/\" [:D, t9:])))] by YELLOW_3: 46;

        

        thus ( sup ( {s} "/\" D)) = ( sup (( proj1 { [s, t]}) "/\" D)) by FUNCT_5: 12

        .= ( sup (( proj1 { [s, t]}) "/\" ( proj1 [:D, t9:]))) by FUNCT_5: 9

        .= ( sup ( proj1 ( { [s, t]} "/\" [:D, t9:]))) by Th24

        .= (( sup ( { [s, t]} "/\" [:D, t9:])) `1 ) by A4

        .= (( [s, t] "/\" ( sup [:D, t9:])) `1 ) by A2

        .= (( [s, t] `1 ) "/\" (( sup [:D, t9:]) `1 )) by Th13

        .= (s "/\" (( sup [:D, t9:]) `1 ))

        .= (s "/\" ( sup ( proj1 [:D, t9:]))) by A3

        .= (s "/\" ( sup D)) by FUNCT_5: 9;

      end;

      thus T is up-complete by A1, WAYBEL_2: 11;

      set s = the Element of S;

      let t be Element of T, D be non empty directed Subset of T;

      reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0: 5;

       ex_sup_of ( [:s9, D:], [:S, T:]) by A1, WAYBEL_0: 75;

      then

       A5: ( sup [:s9, D:]) = [( sup ( proj1 [:s9, D:])), ( sup ( proj2 [:s9, D:]))] by YELLOW_3: 46;

      reconsider ST = { [s, t]} as non empty directed Subset of [:S, T:] by WAYBEL_0: 5;

       ex_sup_of ((ST "/\" [:s9, D:]), [:S, T:]) by A1, WAYBEL_0: 75;

      then

       A6: ( sup ( { [s, t]} "/\" [:s9, D:])) = [( sup ( proj1 ( { [s, t]} "/\" [:s9, D:]))), ( sup ( proj2 ( { [s, t]} "/\" [:s9, D:])))] by YELLOW_3: 46;

      

      thus ( sup ( {t} "/\" D)) = ( sup (( proj2 { [s, t]}) "/\" D)) by FUNCT_5: 12

      .= ( sup (( proj2 { [s, t]}) "/\" ( proj2 [:s9, D:]))) by FUNCT_5: 9

      .= ( sup ( proj2 ( { [s, t]} "/\" [:s9, D:]))) by Th24

      .= (( sup ( { [s, t]} "/\" [:s9, D:])) `2 ) by A6

      .= (( [s, t] "/\" ( sup [:s9, D:])) `2 ) by A2

      .= (( [s, t] `2 ) "/\" (( sup [:s9, D:]) `2 )) by Th13

      .= (t "/\" (( sup [:s9, D:]) `2 ))

      .= (t "/\" ( sup ( proj2 [:s9, D:]))) by A5

      .= (t "/\" ( sup D)) by FUNCT_5: 9;

    end;

    registration

      let S,T be satisfying_axiom_of_approximation up-complete /\-complete non empty Poset;

      cluster [:S, T:] -> satisfying_axiom_of_approximation;

      coherence

      proof

        let x be Element of [:S, T:];

        

         A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

         ex_sup_of (( waybelow x), [:S, T:]) by WAYBEL_0: 75;

        then

         A2: ( sup ( waybelow x)) = [( sup ( proj1 ( waybelow x))), ( sup ( proj2 ( waybelow x)))] by YELLOW_3: 46;

        

        then

         A3: (( sup ( waybelow x)) `2 ) = ( sup ( proj2 ( waybelow x)))

        .= ( sup ( waybelow (x `2 ))) by Th47

        .= (x `2 ) by WAYBEL_3:def 5;

        (( sup ( waybelow x)) `1 ) = ( sup ( proj1 ( waybelow x))) by A2

        .= ( sup ( waybelow (x `1 ))) by Th46

        .= (x `1 ) by WAYBEL_3:def 5;

        hence thesis by A1, A3, DOMAIN_1: 2;

      end;

    end

    registration

      let S,T be continuous /\-complete non empty Poset;

      cluster [:S, T:] -> continuous;

      coherence ;

    end

    theorem :: YELLOW10:68

    for S,T be up-complete lower-bounded non empty Poset st [:S, T:] is continuous holds S is continuous & T is continuous

    proof

      let S,T be up-complete lower-bounded non empty Poset such that

       A1: for x be Element of [:S, T:] holds ( waybelow x) is non empty directed and

       A2: [:S, T:] is up-complete satisfying_axiom_of_approximation;

      hereby

        hereby

          set t = the Element of T;

          let s be Element of S;

          

           A3: ( waybelow [s, t]) is directed by A1;

           [:( waybelow s), ( waybelow t):] = ( waybelow [s, t]) & ( proj1 [:( waybelow s), ( waybelow t):]) = ( waybelow s) by Th44, FUNCT_5: 9;

          hence ( waybelow s) is non empty directed by A3, YELLOW_3: 22;

        end;

        thus S is up-complete;

        thus S is satisfying_axiom_of_approximation

        proof

          set t = the Element of T;

          let s be Element of S;

          ( waybelow [s, t]) is directed by A1;

          then ex_sup_of (( waybelow [s, t]), [:S, T:]) by WAYBEL_0: 75;

          then

           A4: ( sup ( waybelow [s, t])) = [( sup ( proj1 ( waybelow [s, t]))), ( sup ( proj2 ( waybelow [s, t])))] by Th5;

          

          thus s = ( [s, t] `1 )

          .= (( sup ( waybelow [s, t])) `1 ) by A2

          .= ( sup ( proj1 ( waybelow [s, t]))) by A4

          .= ( sup ( waybelow ( [s, t] `1 ))) by Th46

          .= ( sup ( waybelow s));

        end;

      end;

      hereby

        set s = the Element of S;

        let t be Element of T;

        

         A5: ( waybelow [s, t]) is directed by A1;

         [:( waybelow s), ( waybelow t):] = ( waybelow [s, t]) & ( proj2 [:( waybelow s), ( waybelow t):]) = ( waybelow t) by Th44, FUNCT_5: 9;

        hence ( waybelow t) is non empty directed by A5, YELLOW_3: 22;

      end;

      set s = the Element of S;

      thus T is up-complete;

      let t be Element of T;

      now

        let x be Element of [:S, T:];

        ( waybelow x) is non empty directed by A1;

        hence ex_sup_of (( waybelow x), [:S, T:]) by WAYBEL_0: 75;

      end;

      then

       A6: ( sup ( waybelow [s, t])) = [( sup ( proj1 ( waybelow [s, t]))), ( sup ( proj2 ( waybelow [s, t])))] by Th5;

      

      thus t = ( [s, t] `2 )

      .= (( sup ( waybelow [s, t])) `2 ) by A2

      .= ( sup ( proj2 ( waybelow [s, t]))) by A6

      .= ( sup ( waybelow ( [s, t] `2 ))) by Th47

      .= ( sup ( waybelow t));

    end;

    registration

      let S,T be satisfying_axiom_K up-complete lower-bounded sup-Semilattice;

      cluster [:S, T:] -> satisfying_axiom_K;

      coherence

      proof

        let x be Element of [:S, T:];

        

         A1: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by YELLOW_3:def 2;

        

         A2: ( sup ( compactbelow x)) = [( sup ( proj1 ( compactbelow x))), ( sup ( proj2 ( compactbelow x)))] by YELLOW_3: 46;

        

        then

         A3: (( sup ( compactbelow x)) `2 ) = ( sup ( proj2 ( compactbelow x)))

        .= ( sup ( compactbelow (x `2 ))) by Th53

        .= (x `2 ) by WAYBEL_8:def 3;

        (( sup ( compactbelow x)) `1 ) = ( sup ( proj1 ( compactbelow x))) by A2

        .= ( sup ( compactbelow (x `1 ))) by Th52

        .= (x `1 ) by WAYBEL_8:def 3;

        hence thesis by A1, A3, DOMAIN_1: 2;

      end;

    end

    registration

      let S,T be complete algebraic lower-bounded sup-Semilattice;

      cluster [:S, T:] -> algebraic;

      coherence ;

    end

    theorem :: YELLOW10:69

    

     Th69: for S,T be lower-bounded non empty Poset st [:S, T:] is algebraic holds S is algebraic & T is algebraic

    proof

      let S,T be lower-bounded non empty Poset such that

       A1: for x be Element of [:S, T:] holds ( compactbelow x) is non empty directed and

       A2: [:S, T:] is up-complete satisfying_axiom_K;

      

       A3: S is up-complete & T is up-complete by A2, WAYBEL_2: 11;

      hereby

        hereby

          set t = the Element of T;

          let s be Element of S;

          

           A4: ( compactbelow [s, t]) is directed by A1;

           [:( compactbelow s), ( compactbelow t):] = ( compactbelow [s, t]) & ( proj1 [:( compactbelow s), ( compactbelow t):]) = ( compactbelow s) by A3, Th50, FUNCT_5: 9;

          hence ( compactbelow s) is non empty directed by A4, YELLOW_3: 22;

        end;

        thus S is up-complete by A2, WAYBEL_2: 11;

        thus S is satisfying_axiom_K

        proof

          set t = the Element of T;

          let s be Element of S;

          ( compactbelow [s, t]) is non empty directed by A1;

          then ex_sup_of (( compactbelow [s, t]), [:S, T:]) by A2, WAYBEL_0: 75;

          then

           A5: ( sup ( compactbelow [s, t])) = [( sup ( proj1 ( compactbelow [s, t]))), ( sup ( proj2 ( compactbelow [s, t])))] by Th5;

          

          thus s = ( [s, t] `1 )

          .= (( sup ( compactbelow [s, t])) `1 ) by A2

          .= ( sup ( proj1 ( compactbelow [s, t]))) by A5

          .= ( sup ( compactbelow ( [s, t] `1 ))) by A3, Th52

          .= ( sup ( compactbelow s));

        end;

      end;

      set s = the Element of S;

      hereby

        set s = the Element of S;

        let t be Element of T;

        

         A6: ( compactbelow [s, t]) is directed by A1;

         [:( compactbelow s), ( compactbelow t):] = ( compactbelow [s, t]) & ( proj2 [:( compactbelow s), ( compactbelow t):]) = ( compactbelow t) by A3, Th50, FUNCT_5: 9;

        hence ( compactbelow t) is non empty directed by A6, YELLOW_3: 22;

      end;

      thus T is up-complete by A2, WAYBEL_2: 11;

      let t be Element of T;

      ( compactbelow [s, t]) is non empty directed by A1;

      then ex_sup_of (( compactbelow [s, t]), [:S, T:]) by A2, WAYBEL_0: 75;

      then

       A7: ( sup ( compactbelow [s, t])) = [( sup ( proj1 ( compactbelow [s, t]))), ( sup ( proj2 ( compactbelow [s, t])))] by Th5;

      

      thus t = ( [s, t] `2 )

      .= (( sup ( compactbelow [s, t])) `2 ) by A2

      .= ( sup ( proj2 ( compactbelow [s, t]))) by A7

      .= ( sup ( compactbelow ( [s, t] `2 ))) by A3, Th53

      .= ( sup ( compactbelow t));

    end;

    registration

      let S,T be arithmetic lower-bounded LATTICE;

      cluster [:S, T:] -> arithmetic;

      coherence

      proof

        set C = ( CompactSublatt [:S, T:]);

        thus [:S, T:] is algebraic;

        let x,y be Element of [:S, T:] such that

         A1: x in the carrier of C and

         A2: y in the carrier of C and ex_inf_of ( {x, y}, [:S, T:]);

        

         A3: x is compact by A1, WAYBEL_8:def 1;

        then (x `1 ) is compact by Th22;

        then

         A4: (x `1 ) in the carrier of ( CompactSublatt S) by WAYBEL_8:def 1;

        

         A5: y is compact by A2, WAYBEL_8:def 1;

        then (y `1 ) is compact by Th22;

        then

         A6: (y `1 ) in the carrier of ( CompactSublatt S) by WAYBEL_8:def 1;

        (x `2 ) is compact by A3, Th22;

        then

         A7: (x `2 ) in the carrier of ( CompactSublatt T) by WAYBEL_8:def 1;

        (y `2 ) is compact by A5, Th22;

        then

         A8: (y `2 ) in the carrier of ( CompactSublatt T) by WAYBEL_8:def 1;

        ( CompactSublatt T) is meet-inheriting & ex_inf_of ( {(x `2 ), (y `2 )},T) by WAYBEL_8:def 5, YELLOW_0: 21;

        then ( inf {(x `2 ), (y `2 )}) in the carrier of ( CompactSublatt T) by A7, A8;

        then ((x `2 ) "/\" (y `2 )) in the carrier of ( CompactSublatt T) by YELLOW_0: 40;

        then ((x `2 ) "/\" (y `2 )) is compact by WAYBEL_8:def 1;

        then

         A9: ((x "/\" y) `2 ) is compact by Th13;

        ( CompactSublatt S) is meet-inheriting & ex_inf_of ( {(x `1 ), (y `1 )},S) by WAYBEL_8:def 5, YELLOW_0: 21;

        then ( inf {(x `1 ), (y `1 )}) in the carrier of ( CompactSublatt S) by A4, A6;

        then ((x `1 ) "/\" (y `1 )) in the carrier of ( CompactSublatt S) by YELLOW_0: 40;

        then ((x `1 ) "/\" (y `1 )) is compact by WAYBEL_8:def 1;

        then ((x "/\" y) `1 ) is compact by Th13;

        then (x "/\" y) is compact by A9, Th23;

        then ( inf {x, y}) is compact by YELLOW_0: 40;

        hence thesis by WAYBEL_8:def 1;

      end;

    end

    theorem :: YELLOW10:70

    for S,T be lower-bounded LATTICE st [:S, T:] is arithmetic holds S is arithmetic & T is arithmetic

    proof

      let S,T be lower-bounded LATTICE such that

       A1: [:S, T:] is algebraic and

       A2: ( CompactSublatt [:S, T:]) is meet-inheriting;

      

       A3: S is up-complete & T is up-complete by A1, WAYBEL_2: 11;

      hereby

        thus S is algebraic by A1, Th69;

        let x,y be Element of S such that

         A4: x in the carrier of ( CompactSublatt S) and

         A5: y in the carrier of ( CompactSublatt S) and ex_inf_of ( {x, y},S);

        

         A6: ( [y, ( Bottom T)] `1 ) = y & ( [y, ( Bottom T)] `2 ) = ( Bottom T);

        y is compact by A5, WAYBEL_8:def 1;

        then [y, ( Bottom T)] is compact by A3, A6, Th23, WAYBEL_3: 15;

        then

         A7: [y, ( Bottom T)] in the carrier of ( CompactSublatt [:S, T:]) by WAYBEL_8:def 1;

        

         A8: ( [x, ( Bottom T)] `1 ) = x & ( [x, ( Bottom T)] `2 ) = ( Bottom T);

        x is compact by A4, WAYBEL_8:def 1;

        then [x, ( Bottom T)] is compact by A3, A8, Th23, WAYBEL_3: 15;

        then ex_inf_of ( { [x, ( Bottom T)], [y, ( Bottom T)]}, [:S, T:]) & [x, ( Bottom T)] in the carrier of ( CompactSublatt [:S, T:]) by WAYBEL_8:def 1, YELLOW_0: 21;

        then ( inf { [x, ( Bottom T)], [y, ( Bottom T)]}) in the carrier of ( CompactSublatt [:S, T:]) by A2, A7;

        then

         A9: ( inf { [x, ( Bottom T)], [y, ( Bottom T)]}) is compact by WAYBEL_8:def 1;

        (( inf { [x, ( Bottom T)], [y, ( Bottom T)]}) `1 ) = (( [x, ( Bottom T)] "/\" [y, ( Bottom T)]) `1 ) by YELLOW_0: 40

        .= (( [x, ( Bottom T)] `1 ) "/\" ( [y, ( Bottom T)] `1 )) by Th13

        .= (x "/\" ( [y, ( Bottom T)] `1 ))

        .= (x "/\" y);

        then (x "/\" y) is compact by A3, A9, Th22;

        then ( inf {x, y}) is compact by YELLOW_0: 40;

        hence ( inf {x, y}) in the carrier of ( CompactSublatt S) by WAYBEL_8:def 1;

      end;

      thus T is algebraic by A1, Th69;

      let x,y be Element of T such that

       A10: x in the carrier of ( CompactSublatt T) and

       A11: y in the carrier of ( CompactSublatt T) and ex_inf_of ( {x, y},T);

      

       A12: ( [( Bottom S), y] `2 ) = y & ( [( Bottom S), y] `1 ) = ( Bottom S);

      y is compact by A11, WAYBEL_8:def 1;

      then [( Bottom S), y] is compact by A3, A12, Th23, WAYBEL_3: 15;

      then

       A13: [( Bottom S), y] in the carrier of ( CompactSublatt [:S, T:]) by WAYBEL_8:def 1;

      

       A14: ( [( Bottom S), x] `2 ) = x & ( [( Bottom S), x] `1 ) = ( Bottom S);

      x is compact by A10, WAYBEL_8:def 1;

      then [( Bottom S), x] is compact by A3, A14, Th23, WAYBEL_3: 15;

      then ex_inf_of ( { [( Bottom S), x], [( Bottom S), y]}, [:S, T:]) & [( Bottom S), x] in the carrier of ( CompactSublatt [:S, T:]) by WAYBEL_8:def 1, YELLOW_0: 21;

      then ( inf { [( Bottom S), x], [( Bottom S), y]}) in the carrier of ( CompactSublatt [:S, T:]) by A2, A13;

      then

       A15: ( inf { [( Bottom S), x], [( Bottom S), y]}) is compact by WAYBEL_8:def 1;

      (( inf { [( Bottom S), x], [( Bottom S), y]}) `2 ) = (( [( Bottom S), x] "/\" [( Bottom S), y]) `2 ) by YELLOW_0: 40

      .= (( [( Bottom S), x] `2 ) "/\" ( [( Bottom S), y] `2 )) by Th13

      .= (x "/\" ( [( Bottom S), y] `2 ))

      .= (x "/\" y);

      then (x "/\" y) is compact by A3, A15, Th22;

      then ( inf {x, y}) is compact by YELLOW_0: 40;

      hence thesis by WAYBEL_8:def 1;

    end;