The Mizar article:

The Properties of Product of Relational Structures

by
Artur Kornilowicz

Received March 27, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: YELLOW10
[ MML identifier index ]


environ

 vocabulary LATTICES, ORDERS_1, LATTICE3, RELAT_2, YELLOW_0, BOOLE, BHSP_3,
      ORDINAL2, FUNCT_5, MCART_1, WAYBEL_0, WAYBEL_3, QUANTAL1, COMPTS_1,
      WAYBEL_8, WAYBEL_6, WAYBEL11, WAYBEL_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, STRUCT_0, MCART_1, ORDERS_1, LATTICE3,
      YELLOW_0, WAYBEL_0, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_2, WAYBEL_3,
      WAYBEL_6, WAYBEL_8, WAYBEL11;
 constructors YELLOW_4, WAYBEL_1, WAYBEL_3, WAYBEL_6, WAYBEL_8, ORDERS_3,
      WAYBEL11;
 clusters STRUCT_0, LATTICE3, YELLOW_0, YELLOW_3, YELLOW_4, WAYBEL_0, WAYBEL_2,
      WAYBEL_3, WAYBEL_8, WAYBEL14, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, YELLOW_0, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_2,
      WAYBEL_3, WAYBEL_6, WAYBEL_8, WAYBEL11, XBOOLE_0;
 theorems STRUCT_0, ZFMISC_1, TARSKI, ORDERS_1, YELLOW_0, YELLOW_3, YELLOW_4,
      WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3, WAYBEL_8, MCART_1, FUNCT_5,
      DOMAIN_1, XBOOLE_0;

begin  :: On the elements of product of relational structures

definition let S, T be non empty upper-bounded RelStr;
 cluster [:S,T:] -> upper-bounded;
coherence
  proof
    consider s being Element of S such that
A1:   s is_>=_than the carrier of S by YELLOW_0:def 5;
    consider t being Element of T such that
A2:   t is_>=_than the carrier of T by YELLOW_0:def 5;
    take [s,t];
A3: the carrier of [:S,T:] = [:the carrier of S, the carrier of T:]
      by YELLOW_3:def 2;
      the carrier of S c= the carrier of S &
     the carrier of T c= the carrier of T;
    then the carrier of S is Subset of S & the carrier of T is Subset of T
     ;
    hence thesis by A1,A2,A3,YELLOW_3:30;
  end;
end;

definition let S, T be non empty lower-bounded RelStr;
 cluster [:S,T:] -> lower-bounded;
coherence
  proof
    consider s being Element of S such that
A1:   s is_<=_than the carrier of S by YELLOW_0:def 4;
    consider t being Element of T such that
A2:   t is_<=_than the carrier of T by YELLOW_0:def 4;
    take [s,t];
A3: the carrier of [:S,T:] = [:the carrier of S, the carrier of T:]
      by YELLOW_3:def 2;
      the carrier of S c= the carrier of S &
     the carrier of T c= the carrier of T;
    then the carrier of S is Subset of S & the carrier of T is Subset of T
     ;
    hence thesis by A1,A2,A3,YELLOW_3:33;
  end;
end;

theorem
  for S, T being 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 being 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 being set such that
A2:  s in the carrier of S & t in the carrier of T & x = [s,t]
        by ZFMISC_1:def 2;
    reconsider s as Element of S by A2;
    reconsider t as Element of T by A2;
      the carrier of S c= the carrier of S &
     the carrier of T c= the carrier of T;
then A3: the carrier of S is non empty Subset of S &
     the carrier of T is non empty Subset of T;
A4: [s,t] is_>=_than [:the carrier of S,the carrier of T:]
      by A1,A2,YELLOW_3:def 2;
    thus S is upper-bounded
    proof
      take s;
      thus thesis by A3,A4,YELLOW_3:29;
    end;
    take t;
    thus thesis by A3,A4,YELLOW_3:29;
  end;

theorem
  for S, T being 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 being 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 being set such that
A2:  s in the carrier of S & t in the carrier of T & x = [s,t]
        by ZFMISC_1:def 2;
    reconsider s as Element of S by A2;
    reconsider t as Element of T by A2;
      the carrier of S c= the carrier of S &
     the carrier of T c= the carrier of T;
then A3: the carrier of S is non empty Subset of S &
     the carrier of T is non empty Subset of T;
A4: [s,t] is_<=_than [:the carrier of S,the carrier of T:]
      by A1,A2,YELLOW_3:def 2;
    thus S is lower-bounded
    proof
      take s;
      thus thesis by A3,A4,YELLOW_3:32;
    end;
    take t;
    thus thesis by A3,A4,YELLOW_3:32;
  end;

theorem Th3:
for S, T being 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: ex_inf_of {},[:S,T:] by YELLOW_0:43;
A2: {} is_>=_than [Top S,Top T] by YELLOW_0:6;
      for a being 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 being set such that
A3:     s in the carrier of S & t in the carrier of T & a = [s,t]
          by ZFMISC_1:def 2;
      reconsider s as Element of S by A3;
      reconsider t as Element of T by A3;
        s <= Top S & t <= Top T by YELLOW_0:45;
      hence a <= [Top S,Top T] by A3,YELLOW_3:11;
    end;
    then [Top S,Top T] = "/\"({},[:S,T:]) by A1,A2,YELLOW_0:def 10;
    hence Top [:S,T:] = [Top S,Top T] by YELLOW_0:def 12;
  end;

theorem Th4:
for S, T being 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: ex_sup_of {},[:S,T:] by YELLOW_0:42;
A2: {} is_<=_than [Bottom S,Bottom T] by YELLOW_0:6;
      for a being 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 being set such that
A3:     s in the carrier of S & t in the carrier of T & a = [s,t]
          by ZFMISC_1:def 2;
      reconsider s as Element of S by A3;
      reconsider t as Element of T by A3;
        Bottom S <= s & Bottom T <= t by YELLOW_0:44;
      hence [Bottom S,Bottom T] <= a by A3,YELLOW_3:11;
    end;
    then [Bottom S,Bottom T] = "\/"({},[:S,T:]) by A1,A2,YELLOW_0:def 9;
    hence Bottom [:S,T:] = [Bottom S,Bottom T] by YELLOW_0:def 11;
  end;

theorem Th5:
for S, T being lower-bounded antisymmetric non empty RelStr,
    D being 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;
    suppose D = {};
    then sup D = Bottom [:S,T:] & sup proj1 D = Bottom S & sup proj2 D =
Bottom T
      by FUNCT_5:10,YELLOW_0:def 11;
    hence [sup proj1 D,sup proj2 D] = sup D by Th4;
  end;

theorem
  for S, T being upper-bounded antisymmetric (non empty RelStr),
    D being 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;
    suppose D = {};
    then inf D = Top [:S,T:] & inf proj1 D = Top S & inf proj2 D = Top T
      by FUNCT_5:10,YELLOW_0:def 12;
    hence [inf proj1 D,inf proj2 D] = inf D by Th3;
  end;

theorem
  for S, T being non empty RelStr,
    x, y being 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
      assume
A1:     for b being Element of [:S,T:] st b in {y} 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:23;
      then [y`1,y`2] in {y} by TARSKI:def 1;
then A3:   x <= [y`1,y`2] by A1;
A4:   x = [x`1,x`2] by A2,MCART_1:23;
      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 A3,A4,YELLOW_3:11;
      end;
      let b be Element of T;
      assume b in {y`2};
      then b = y`2 by TARSKI:def 1;
      hence x`2 <= b by A3,A4,YELLOW_3:11;
    end;
    assume that
A5:   for b being Element of S st b in {y`1} holds x`1 <= b and
A6:   for b being Element of T st b in {y`2} holds x`2 <= b;
    let b be Element of [:S,T:];
    assume b in {y};
    then b = y by TARSKI:def 1;
    then b`1 in {y`1} & b`2 in {y`2} by TARSKI:def 1;
    then x`1 <= b`1 & x`2 <= b`2 by A5,A6;
    hence x <= b by YELLOW_3:12;
  end;

theorem
  for S, T being non empty RelStr,
    x, y, z being 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 being 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] & z = [z`1,z`2] by MCART_1:23;
      then [y`1,y`2] in {y,z} & [z`1,z`2] in {y,z} by TARSKI:def 2;
then A3:   x <= [y`1,y`2] & x <= [z`1,z`2] by A1;
A4:   x = [x`1,x`2] by A2,MCART_1:23;
      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,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 x`2 <= b by A3,A4,YELLOW_3:11;
    end;
    assume that
A5:   for b being Element of S st b in {y`1,z`1} holds x`1 <= b and
A6:   for b being 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 b = y or b = z by TARSKI:def 2;
    then b`1 in {y`1,z`1} & b`2 in {y`2,z`2} by TARSKI:def 2;
    then x`1 <= b`1 & x`2 <= b`2 by A5,A6;
    hence x <= b by YELLOW_3:12;
  end;

theorem
  for S, T being non empty RelStr,
    x, y being 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
      assume
A1:     for b being Element of [:S,T:] st b in {y} 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:23;
      then [y`1,y`2] in {y} by TARSKI:def 1;
then A3:   x >= [y`1,y`2] by A1;
A4:   x = [x`1,x`2] by A2,MCART_1:23;
      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 A3,A4,YELLOW_3:11;
      end;
      let b be Element of T;
      assume b in {y`2};
      then b = y`2 by TARSKI:def 1;
      hence x`2 >= b by A3,A4,YELLOW_3:11;
    end;
    assume that
A5:   for b being Element of S st b in {y`1} holds x`1 >= b and
A6:   for b being Element of T st b in {y`2} holds x`2 >= b;
    let b be Element of [:S,T:];
    assume b in {y};
    then b = y by TARSKI:def 1;
    then b`1 in {y`1} & b`2 in {y`2} by TARSKI:def 1;
    then x`1 >= b`1 & x`2 >= b`2 by A5,A6;
    hence x >= b by YELLOW_3:12;
  end;

theorem
  for S, T being non empty RelStr,
    x, y, z being 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 being 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] & z = [z`1,z`2] by MCART_1:23;
      then [y`1,y`2] in {y,z} & [z`1,z`2] in {y,z} by TARSKI:def 2;
then A3:   x >= [y`1,y`2] & x >= [z`1,z`2] by A1;
A4:   x = [x`1,x`2] by A2,MCART_1:23;
      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,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 x`2 >= b by A3,A4,YELLOW_3:11;
    end;
    assume that
A5:   for b being Element of S st b in {y`1,z`1} holds x`1 >= b and
A6:   for b being 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 b = y or b = z by TARSKI:def 2;
    then b`1 in {y`1,z`1} & b`2 in {y`2,z`2} by TARSKI:def 2;
    then x`1 >= b`1 & x`2 >= b`2 by A5,A6;
    hence x >= b by YELLOW_3:12;
  end;

theorem
  for S, T being non empty antisymmetric RelStr,
    x, y being 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:23;
    then proj1 {x,y} = {x`1,y`1} & proj2 {x,y} = {x`2,y`2} by FUNCT_5:16;
    hence thesis by YELLOW_3:42;
  end;

theorem
  for S, T being non empty antisymmetric RelStr,
    x, y being 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:23;
    then proj1 {x,y} = {x`1,y`1} & proj2 {x,y} = {x`2,y`2} by FUNCT_5:16;
    hence thesis by YELLOW_3:41;
  end;

theorem Th13:
for S, T being with_infima antisymmetric RelStr,
    x, y being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23;
    set a = (x "/\" y)`1,
        b = (x "/\" y)`2;
      x "/\" y <= x & x "/\" y <= y by YELLOW_0:23;
then A2: a <= x`1 & a <= y`1 & b <= x`2 & b <= y`2 by YELLOW_3:12;
A3: for d being Element of S st d <= x`1 & d <= y`1 holds a >= d
    proof
      let d be Element of S such that
A4:     d <= x`1 & d <= y`1;
      set t = x`2 "/\" y`2;
        t <= x`2 & t <= y`2 by YELLOW_0:23;
      then [d,t] <= x & [d,t] <= y by A1,A4,YELLOW_3:11;
then A5:   x "/\" y >= [d,t] by YELLOW_0:23;
        [d,t]`1 = d by MCART_1:7;
      hence a >= d by A5,YELLOW_3:12;
    end;
      for d being Element of T st d <= x`2 & d <= y`2 holds b >= d
    proof
      let d be Element of T such that
A6:     d <= x`2 & d <= y`2;
      set s = x`1 "/\" y`1;
        s <= x`1 & s <= y`1 by YELLOW_0:23;
      then [s,d] <= x & [s,d] <= y by A1,A6,YELLOW_3:11;
then A7:   x "/\" y >= [s,d] by YELLOW_0:23;
        [s,d]`2 = d by MCART_1:7;
      hence b >= d by A7,YELLOW_3:12;
    end;
    hence thesis by A2,A3,YELLOW_0:19;
  end;

theorem Th14:
for S, T being with_suprema antisymmetric RelStr,
    x, y being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] & y = [y`1,y`2] by MCART_1:23;
    set a = (x "\/" y)`1,
        b = (x "\/" y)`2;
      x "\/" y >= x & x "\/" y >= y by YELLOW_0:22;
then A2: a >= x`1 & a >= y`1 & b >= x`2 & b >= y`2 by YELLOW_3:12;
A3: for d being Element of S st d >= x`1 & d >= y`1 holds a <= d
    proof
      let d be Element of S such that
A4:     d >= x`1 & d >= y`1;
      set t = x`2 "\/" y`2;
        t >= x`2 & t >= y`2 by YELLOW_0:22;
      then [d,t] >= x & [d,t] >= y by A1,A4,YELLOW_3:11;
then A5:   x "\/" y <= [d,t] by YELLOW_0:22;
        [d,t]`1 = d by MCART_1:7;
      hence a <= d by A5,YELLOW_3:12;
    end;
      for d being Element of T st d >= x`2 & d >= y`2 holds b <= d
    proof
      let d be Element of T such that
A6:     d >= x`2 & d >= y`2;
      set s = x`1 "\/" y`1;
        s >= x`1 & s >= y`1 by YELLOW_0:22;
      then [s,d] >= x & [s,d] >= y by A1,A6,YELLOW_3:11;
then A7:   x "\/" y <= [s,d] by YELLOW_0:22;
        [s,d]`2 = d by MCART_1:7;
      hence b <= d by A7,YELLOW_3:12;
    end;
    hence thesis by A2,A3,YELLOW_0:18;
  end;

theorem Th15:
for S, T being with_infima antisymmetric RelStr,
    x1, y1 being Element of S,
    x2, y2 being 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])`1 = [x1,x2]`1 "/\" [y1,y2]`1 by Th13
                          .= x1 "/\" [y1,y2]`1 by MCART_1:7
                          .= x1 "/\" y1 by MCART_1:7
                          .= [x1 "/\" y1, x2 "/\" y2]`1 by MCART_1:7;
      ([x1,x2] "/\" [y1,y2])`2 = [x1,x2]`2 "/\" [y1,y2]`2 by Th13
                          .= x2 "/\" [y1,y2]`2 by MCART_1:7
                          .= x2 "/\" y2 by MCART_1:7
                          .= [x1 "/\" y1, x2 "/\" y2]`2 by MCART_1:7;
    hence thesis by A1,A2,DOMAIN_1:12;
  end;

theorem Th16:
for S, T being with_suprema antisymmetric RelStr,
    x1, y1 being Element of S,
    x2, y2 being 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])`1 = [x1,x2]`1 "\/" [y1,y2]`1 by Th14
                          .= x1 "\/" [y1,y2]`1 by MCART_1:7
                          .= x1 "\/" y1 by MCART_1:7
                          .= [x1 "\/" y1, x2 "\/" y2]`1 by MCART_1:7;
      ([x1,x2] "\/" [y1,y2])`2 = [x1,x2]`2 "\/" [y1,y2]`2 by Th14
                          .= x2 "\/" [y1,y2]`2 by MCART_1:7
                          .= x2 "\/" y2 by MCART_1:7
                          .= [x1 "\/" y1, x2 "\/" y2]`2 by MCART_1:7;
    hence thesis by A1,A2,DOMAIN_1:12;
  end;

definition let S be with_suprema with_infima antisymmetric RelStr,
               x, y be Element of S;
 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 by WAYBEL_1:def 23;
  end;
end;

theorem Th17:
for S, T being bounded with_suprema with_infima antisymmetric RelStr,
    x, y being 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:];
    hereby
      assume
A1:     x is_a_complement_of y;
      thus x`1 is_a_complement_of y`1
      proof
        thus y`1 "\/" x`1
           = (y "\/" x)`1 by Th14
          .= (Top [:S,T:])`1 by A1,WAYBEL_1:def 23
          .= [Top S,Top T]`1 by Th3
          .= Top S by MCART_1:7;
        thus y`1 "/\" x`1
           = (y "/\" x)`1 by Th13
          .= (Bottom [:S,T:])`1 by A1,WAYBEL_1:def 23
          .= [Bottom S,Bottom T]`1 by Th4
          .= Bottom S by MCART_1:7;
      end;
      thus x`2 is_a_complement_of y`2
      proof
        thus y`2 "\/" x`2
           = (y "\/" x)`2 by Th14
          .= (Top [:S,T:])`2 by A1,WAYBEL_1:def 23
          .= [Top S,Top T]`2 by Th3
          .= Top T by MCART_1:7;
        thus y`2 "/\" x`2
           = (y "/\" x)`2 by Th13
          .= (Bottom [:S,T:])`2 by A1,WAYBEL_1:def 23
          .= [Bottom S,Bottom T]`2 by Th4
          .= Bottom T by MCART_1:7;
      end;
    end;
A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    assume that
A3:   y`1 "\/" x`1 = Top S and
A4:   y`1 "/\" x`1 = Bottom S and
A5:   y`2 "\/" x`2 = Top T and
A6:   y`2 "/\" x`2 = Bottom T;
A7: (y "\/" x)`1 = y`1 "\/" x`1 by Th14
              .= [Top S,Top T]`1 by A3,MCART_1:7;
      (y "\/" x)`2 = y`2 "\/" x`2 by Th14
              .= [Top S,Top T]`2 by A5,MCART_1:7;
    hence y "\/" x = [Top S,Top T] by A2,A7,DOMAIN_1:12
                .= Top [:S,T:] by Th3;
A8: (y "/\" x)`1 = y`1 "/\" x`1 by Th13
              .= [Bottom S,Bottom T]`1 by A4,MCART_1:7;
      (y "/\" x)`2 = y`2 "/\" x`2 by Th13
              .= [Bottom S,Bottom T]`2 by A6,MCART_1:7;
    hence y "/\" x = [Bottom S,Bottom T] by A2,A8,DOMAIN_1:12
                .= Bottom [:S,T:] by Th4;
  end;

theorem Th18:
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    a, c being Element of S, b, d being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    assume
A2:   for D being non empty directed Subset of [:S,T:] st [c,d] <= sup D
        ex e being Element of [:S,T:] st e in D & [a,b] <= e;
    thus a << c
    proof
      let D be non empty directed Subset of S such that
A3:     c <= sup D;
      reconsider d' = {d} as non empty directed Subset of T by WAYBEL_0:5;
        ex_sup_of D,S & ex_sup_of d',T by WAYBEL_0:75;
then A4:   sup [:D,d':] = [sup D,sup d'] by YELLOW_3:43;
        d <= sup d' by YELLOW_0:39;
      then [c,d] <= sup [:D,d':] by A3,A4,YELLOW_3:11;
      then consider e being Element of [:S,T:] such that
A5:     e in [:D,d':] & [a,b] <= e by A2;
      take e`1;
      thus e`1 in D by A5,MCART_1:10;
        e = [e`1,e`2] by A1,MCART_1:23;
      hence a <= e`1 by A5,YELLOW_3:11;
    end;
    let D be non empty directed Subset of T such that
A6:   d <= sup D;
    reconsider c' = {c} as non empty directed Subset of S by WAYBEL_0:5;
      ex_sup_of c',S & ex_sup_of D,T by WAYBEL_0:75;
then A7: sup [:c',D:] = [sup c',sup D] by YELLOW_3:43;
      c <= sup c' by YELLOW_0:39;
    then [c,d] <= sup [:c',D:] by A6,A7,YELLOW_3:11;
    then consider e being Element of [:S,T:] such that
A8:   e in [:c',D:] & [a,b] <= e by A2;
    take e`2;
    thus e`2 in D by A8,MCART_1:10;
      e = [e`1,e`2] by A1,MCART_1:23;
    hence b <= e`2 by A8,YELLOW_3:11;
  end;

theorem Th19:
for S, T being up-complete (non empty Poset)
 for a, c being Element of S, b, d being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    assume
A2:  for D being non empty directed Subset of S st c <= sup D
      ex e being Element of S st e in D & a <= e;
    assume
A3:  for D being non empty directed Subset of T st d <= sup D
      ex e being Element of T st e in D & b <= e;
    let D be non empty directed Subset of [:S,T:] such that
A4:   [c,d] <= sup D;
A5: proj1 D is non empty directed & proj2 D is non empty directed
      by YELLOW_3:21,22;
      ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A6: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
    then c <= sup proj1 D by A4,YELLOW_3:11;
    then consider e being Element of S such that
A7:   e in proj1 D & a <= e by A2,A5;
      d <= sup proj2 D by A4,A6,YELLOW_3:11;
    then consider f being Element of T such that
A8:   f in proj2 D & b <= f by A3,A5;
    consider e2 being set such that
A9:   [e,e2] in D by A7,FUNCT_5:def 1;
    consider f1 being set such that
A10:   [f1,f] in D by A8,FUNCT_5:def 2;
      e2 in the carrier of T by A1,A9,ZFMISC_1:106;
    then reconsider e2 as Element of T;
      f1 in the carrier of S by A1,A10,ZFMISC_1:106;
    then reconsider f1 as Element of S;
    consider ef being Element of [:S,T:] such that
A11: ef in D & [e,e2] <= ef & [f1,f] <= ef by A9,A10,WAYBEL_0:def 1;
    take ef;
    thus ef in D by A11;
A12: [a,b] <= [e,f] by A7,A8,YELLOW_3:11;
A13: ef = [ef`1,ef`2] by A1,MCART_1:23;
    then e <= ef`1 & f <= ef`2 by A11,YELLOW_3:11;
    then [e,f] <= ef by A13,YELLOW_3:11;
    hence [a,b] <= ef by A12,ORDERS_1:26;
  end;

theorem Th20:
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x, y being 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:23;
    hence x`1 << y`1 & x`2 << y`2 by A1,Th18;
  end;

theorem Th21:
for S, T being up-complete (non empty Poset),
    x, y being 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:23;
    hence thesis by Th19;
  end;

theorem Th22:
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being 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 Th23:
for S, T being up-complete (non empty Poset),
    x being 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  :: On the subsets of product of relational structures

theorem Th24:
for S, T being with_infima antisymmetric RelStr,
    X, Y being 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 is 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 is Element of S:
      x in proj1 X & y in proj1 Y } by YELLOW_4:def 4;
    hereby
      hereby
        let a be set;
        assume a in proj1 (X "/\" Y);
        then consider b being set such that
A4:       [a,b] in X "/\" Y by FUNCT_5:def 1;
        consider x, y being Element of [:S,T:] such that
A5:       [a,b] = x "/\" y and
A6:       x in X & y in Y by A2,A4;
A7:     a = [a,b]`1 by MCART_1:7
         .= x`1 "/\" y`1 by A5,Th13;
          x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23;
        then x`1 in proj1 X & y`1 in proj1 Y by A6,FUNCT_5:4;
        hence a in proj1 X "/\" proj1 Y by A7,YELLOW_4:37;
      end;
      let a be set;
      assume a in proj1 X "/\" proj1 Y;
      then consider x, y being Element of S such that
A8:     a = x "/\" y & x in proj1 X & y in proj1 Y by A3;
      consider x2 being set such that
A9:     [x,x2] in X by A8,FUNCT_5:def 1;
      consider y2 being set such that
A10:     [y,y2] in Y by A8,FUNCT_5:def 1;
        x2 in the carrier of T & y2 in the carrier of T
        by A1,A9,A10,ZFMISC_1:106;
      then reconsider x2, y2 as Element of T;
        [x,x2] "/\" [y,y2] = [a,x2 "/\" y2] by A8,Th15;
      then [a,x2 "/\" y2] in X "/\" Y by A9,A10,YELLOW_4:37;
      hence a in proj1 (X "/\" Y) by FUNCT_5:def 1;
    end;
A11: proj2 X "/\" proj2 Y = { x "/\" y where x, y is Element of T:
      x in proj2 X & y in proj2 Y } by YELLOW_4:def 4;
    hereby
      let b be set;
      assume b in proj2 (X "/\" Y);
      then consider a being set such that
A12:     [a,b] in X "/\" Y by FUNCT_5:def 2;
      consider x, y being Element of [:S,T:] such that
A13:     [a,b] = x "/\" y and
A14:     x in X & y in Y by A2,A12;
A15:   b = [a,b]`2 by MCART_1:7
       .= x`2 "/\" y`2 by A13,Th13;
        x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23;
      then x`2 in proj2 X & y`2 in proj2 Y by A14,FUNCT_5:4;
      hence b in proj2 X "/\" proj2 Y by A15,YELLOW_4:37;
    end;
    let b be set;
    assume b in proj2 X "/\" proj2 Y;
    then consider x, y being Element of T such that
A16:     b = x "/\" y & x in proj2 X & y in proj2 Y by A11;
    consider x1 being set such that
A17:     [x1,x] in X by A16,FUNCT_5:def 2;
    consider y1 being set such that
A18:     [y1,y] in Y by A16,FUNCT_5:def 2;
      x1 in the carrier of S & y1 in the carrier of S
      by A1,A17,A18,ZFMISC_1:106;
    then reconsider x1, y1 as Element of S;
      [x1,x] "/\" [y1,y] = [x1 "/\" y1,b] by A16,Th15;
    then [x1 "/\" y1,b] in X "/\" Y by A17,A18,YELLOW_4:37;
    hence b in proj2 (X "/\" Y) by FUNCT_5:def 2;
  end;

theorem
  for S, T being with_suprema antisymmetric RelStr,
    X, Y being 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 is 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 is Element of S:
      x in proj1 X & y in proj1 Y } by YELLOW_4:def 3;
    hereby
      hereby
        let a be set;
        assume a in proj1 (X "\/" Y);
        then consider b being set such that
A4:       [a,b] in X "\/" Y by FUNCT_5:def 1;
        consider x, y being Element of [:S,T:] such that
A5:       [a,b] = x "\/" y and
A6:       x in X & y in Y by A2,A4;
A7:     a = [a,b]`1 by MCART_1:7
         .= x`1 "\/" y`1 by A5,Th14;
          x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23;
        then x`1 in proj1 X & y`1 in proj1 Y by A6,FUNCT_5:4;
        hence a in proj1 X "\/" proj1 Y by A7,YELLOW_4:10;
      end;
      let a be set;
      assume a in proj1 X "\/" proj1 Y;
      then consider x, y being Element of S such that
A8:     a = x "\/" y & x in proj1 X & y in proj1 Y by A3;
      consider x2 being set such that
A9:     [x,x2] in X by A8,FUNCT_5:def 1;
      consider y2 being set such that
A10:     [y,y2] in Y by A8,FUNCT_5:def 1;
        x2 in the carrier of T & y2 in the carrier of T
        by A1,A9,A10,ZFMISC_1:106;
      then reconsider x2, y2 as Element of T;
        [x,x2] "\/" [y,y2] = [a,x2 "\/" y2] by A8,Th16;
      then [a,x2 "\/" y2] in X "\/" Y by A9,A10,YELLOW_4:10;
      hence a in proj1 (X "\/" Y) by FUNCT_5:def 1;
    end;
A11: proj2 X "\/" proj2 Y = { x "\/" y where x, y is Element of T:
      x in proj2 X & y in proj2 Y } by YELLOW_4:def 3;
    hereby
      let b be set;
      assume b in proj2 (X "\/" Y);
      then consider a being set such that
A12:     [a,b] in X "\/" Y by FUNCT_5:def 2;
      consider x, y being Element of [:S,T:] such that
A13:     [a,b] = x "\/" y and
A14:     x in X & y in Y by A2,A12;
A15:   b = [a,b]`2 by MCART_1:7
       .= x`2 "\/" y`2 by A13,Th14;
        x = [x`1,x`2] & y = [y`1,y`2] by A1,MCART_1:23;
      then x`2 in proj2 X & y`2 in proj2 Y by A14,FUNCT_5:4;
      hence b in proj2 X "\/" proj2 Y by A15,YELLOW_4:10;
    end;
    let b be set;
    assume b in proj2 X "\/" proj2 Y;
    then consider x, y being Element of T such that
A16:     b = x "\/" y & x in proj2 X & y in proj2 Y by A11;
    consider x1 being set such that
A17:     [x1,x] in X by A16,FUNCT_5:def 2;
    consider y1 being set such that
A18:     [y1,y] in Y by A16,FUNCT_5:def 2;
      x1 in the carrier of S & y1 in the carrier of S
      by A1,A17,A18,ZFMISC_1:106;
    then reconsider x1, y1 as Element of S;
      [x1,x] "\/" [y1,y] = [x1 "\/" y1,b] by A16,Th16;
    then [x1 "\/" y1,b] in X "\/" Y by A17,A18,YELLOW_4:10;
    hence b in proj2 (X "\/" Y) by FUNCT_5:def 2;
  end;

theorem
  for S, T being RelStr, X being 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:];
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    let x be set; assume
A2:   x in downarrow X;
    then consider a, b being set such that
A3:   a in the carrier of S & b in the carrier of T and x = [a,b]
       by A1,ZFMISC_1:def 2;
    reconsider S' = S, T' = T as non empty RelStr by A3,STRUCT_0:def 1;
    reconsider x' = x as Element of [:S',T':] by A2;
    consider y being Element of [:S',T':] such that
A4:   y >= x' & y in X by A2,WAYBEL_0:def 15;
A5: y`1 >= x'`1 & y`2 >= x'`2 by A4,YELLOW_3:12;
      y = [y`1,y`2] by A1,MCART_1:23;
    then y`1 in proj1 X & y`2 in proj2 X by A4,FUNCT_5:4;
then A6: x`1 in downarrow proj1 X & x`2 in
 downarrow proj2 X by A5,WAYBEL_0:def 15;
      x' = [x'`1,x'`2] by A1,MCART_1:23;
    hence x in [:downarrow proj1 X,downarrow proj2 X:] by A6,MCART_1:11;
  end;

theorem
  for S, T being RelStr, X being Subset of S, Y being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    hereby
      let x be set;
      assume x in [:downarrow X,downarrow Y:];
      then consider x1, x2 being set such that
A2:     x1 in downarrow X & x2 in downarrow Y & x = [x1,x2]
          by ZFMISC_1:def 2;
      reconsider S' = S, T' = T as non empty RelStr by A2,STRUCT_0:def 1;
      reconsider x1 as Element of S' by A2;
      reconsider x2 as Element of T' by A2;
      consider y1 being Element of S' such that
A3:     y1 >= x1 & y1 in X by A2,WAYBEL_0:def 15;
      consider y2 being Element of T' such that
A4:     y2 >= x2 & y2 in Y by A2,WAYBEL_0:def 15;
A5:   [y1,y2] in [:X,Y:] by A3,A4,ZFMISC_1:106;
        [y1,y2] >= [x1,x2] by A3,A4,YELLOW_3:11;
      hence x in downarrow [:X,Y:] by A2,A5,WAYBEL_0:def 15;
    end;
    let x be set; assume
A6:   x in downarrow [:X,Y:];
    then consider a, b being set such that
A7:   a in the carrier of S & b in the carrier of T and x = [a,b]
       by A1,ZFMISC_1:def 2;
    reconsider S' = S, T' = T as non empty RelStr by A7,STRUCT_0:def 1;
    reconsider x' = x as Element of [:S',T':] by A6;
    consider y being Element of [:S',T':] such that
A8:   y >= x' & y in [:X,Y:] by A6,WAYBEL_0:def 15;
A9: y`1 >= x'`1 & y`2 >= x'`2 by A8,YELLOW_3:12;
      y`1 in X & y`2 in Y by A8,MCART_1:10;
then A10: x`1 in downarrow X & x`2 in downarrow Y by A9,WAYBEL_0:def 15;
      x' = [x'`1,x'`2] by A1,MCART_1:23;
    hence x in [:downarrow X,downarrow Y:] by A10,MCART_1:11;
  end;

theorem Th28:
for S, T being RelStr, X being 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 set;
      assume a in proj1 downarrow X;
      then consider b being set such that
A2:     [a,b] in downarrow X by FUNCT_5:def 1;
A3:   a in the carrier of S & b in the carrier of T by A1,A2,ZFMISC_1:106;
      then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1;
      reconsider a' = a as Element of S' by A3;
      reconsider b' = b as Element of T' by A3;
      consider c being Element of [:S',T':] such that
A4:     [a',b'] <= c & c in X by A2,WAYBEL_0:def 15;
A5:   c = [c`1,c`2] by A1,MCART_1:23;
then A6:   a' <= c`1 by A4,YELLOW_3:11;
        c`1 in proj1 X by A4,A5,FUNCT_5:4;
      hence a in downarrow proj1 X by A6,WAYBEL_0:def 15;
    end;
    let b be set;
    assume b in proj2 downarrow X;
    then consider a being set such that
A7:   [a,b] in downarrow X by FUNCT_5:def 2;
A8: a in the carrier of S & b in the carrier of T by A1,A7,ZFMISC_1:106;
    then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1;
    reconsider a' = a as Element of S' by A8;
    reconsider b' = b as Element of T' by A8;
    consider c being Element of [:S',T':] such that
A9:   [a',b'] <= c & c in X by A7,WAYBEL_0:def 15;
A10: c = [c`1,c`2] by A1,MCART_1:23;
then A11: b' <= c`2 by A9,YELLOW_3:11;
      c`2 in proj2 X by A9,A10,FUNCT_5:4;
    hence b in downarrow proj2 X by A11,WAYBEL_0:def 15;
  end;

theorem
  for S being RelStr, T being reflexive RelStr, X being 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:];
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    thus proj1 downarrow X c= downarrow proj1 X by Th28;
    let a be set; assume
A2:   a in downarrow proj1 X;
    then reconsider S' = S as non empty RelStr by STRUCT_0:def 1;
    reconsider a' = a as Element of S' by A2;
    consider b being Element of S' such that
A3:   b >= a' & b in proj1 X by A2,WAYBEL_0:def 15;
    consider b2 being set such that
A4:   [b,b2] in X by A3,FUNCT_5:def 1;
A5: b2 in the carrier of T by A1,A4,ZFMISC_1:106;
    then reconsider T' = T as non empty reflexive RelStr by STRUCT_0:def 1;
    reconsider b2 as Element of T' by A5;
      b2 <= b2;
    then [b,b2] >= [a',b2] by A3,YELLOW_3:11;
    then [a',b2] in downarrow X by A4,WAYBEL_0:def 15;
    hence a in proj1 downarrow X by FUNCT_5:def 1;
  end;

theorem
  for S being reflexive RelStr, T being RelStr, X being 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:];
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    thus proj2 downarrow X c= downarrow proj2 X by Th28;
    let c be set; assume
A2:   c in downarrow proj2 X;
    then reconsider T' = T as non empty RelStr by STRUCT_0:def 1;
    reconsider c' = c as Element of T' by A2;
    consider b being Element of T' such that
A3:   b >= c' & b in proj2 X by A2,WAYBEL_0:def 15;
    consider b1 being set such that
A4:   [b1,b] in X by A3,FUNCT_5:def 2;
A5: b1 in the carrier of S by A1,A4,ZFMISC_1:106;
    then reconsider S' = S as non empty reflexive RelStr by STRUCT_0:def 1;
    reconsider b1 as Element of S' by A5;
      b1 <= b1;
    then [b1,b] >= [b1,c'] by A3,YELLOW_3:11;
    then [b1,c'] in downarrow X by A4,WAYBEL_0:def 15;
    hence c in proj2 downarrow X by FUNCT_5:def 2;
  end;

theorem
  for S, T being RelStr, X being 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:];
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    let x be set; assume
A2:   x in uparrow X;
    then consider a, b being set such that
A3:   a in the carrier of S & b in the carrier of T and x = [a,b]
       by A1,ZFMISC_1:def 2;
    reconsider S' = S, T' = T as non empty RelStr by A3,STRUCT_0:def 1;
    reconsider x' = x as Element of [:S',T':] by A2;
    consider y being Element of [:S',T':] such that
A4:   y <= x' & y in X by A2,WAYBEL_0:def 16;
A5: y`1 <= x'`1 & y`2 <= x'`2 by A4,YELLOW_3:12;
      y = [y`1,y`2] by A1,MCART_1:23;
    then y`1 in proj1 X & y`2 in proj2 X by A4,FUNCT_5:4;
then A6: x`1 in uparrow proj1 X & x`2 in uparrow proj2 X by A5,WAYBEL_0:def 16;
      x' = [x'`1,x'`2] by A1,MCART_1:23;
    hence x in [:uparrow proj1 X,uparrow proj2 X:] by A6,MCART_1:11;
  end;

theorem
  for S, T being RelStr, X being Subset of S, Y being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    hereby
      let x be set;
      assume x in [:uparrow X,uparrow Y:];
      then consider x1, x2 being set such that
A2:     x1 in uparrow X & x2 in uparrow Y & x = [x1,x2]
          by ZFMISC_1:def 2;
      reconsider S' = S, T' = T as non empty RelStr by A2,STRUCT_0:def 1;
      reconsider x1 as Element of S' by A2;
      reconsider x2 as Element of T' by A2;
      consider y1 being Element of S' such that
A3:     y1 <= x1 & y1 in X by A2,WAYBEL_0:def 16;
      consider y2 being Element of T' such that
A4:     y2 <= x2 & y2 in Y by A2,WAYBEL_0:def 16;
A5:   [y1,y2] in [:X,Y:] by A3,A4,ZFMISC_1:106;
        [y1,y2] <= [x1,x2] by A3,A4,YELLOW_3:11;
      hence x in uparrow [:X,Y:] by A2,A5,WAYBEL_0:def 16;
    end;
    let x be set; assume
A6:   x in uparrow [:X,Y:];
    then consider a, b being set such that
A7:   a in the carrier of S & b in the carrier of T and x = [a,b]
       by A1,ZFMISC_1:def 2;
    reconsider S' = S, T' = T as non empty RelStr by A7,STRUCT_0:def 1;
    reconsider x' = x as Element of [:S',T':] by A6;
    consider y being Element of [:S',T':] such that
A8:   y <= x' & y in [:X,Y:] by A6,WAYBEL_0:def 16;
A9: y`1 <= x'`1 & y`2 <= x'`2 by A8,YELLOW_3:12;
      y`1 in X & y`2 in Y by A8,MCART_1:10;
then A10: x`1 in uparrow X & x`2 in uparrow Y by A9,WAYBEL_0:def 16;
      x' = [x'`1,x'`2] by A1,MCART_1:23;
    hence x in [:uparrow X,uparrow Y:] by A10,MCART_1:11;
  end;

theorem Th33:
for S, T being RelStr, X being 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 set;
      assume a in proj1 uparrow X;
      then consider b being set such that
A2:     [a,b] in uparrow X by FUNCT_5:def 1;
A3:   a in the carrier of S & b in the carrier of T by A1,A2,ZFMISC_1:106;
      then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1;
      reconsider a' = a as Element of S' by A3;
      reconsider b' = b as Element of T' by A3;
      consider c being Element of [:S',T':] such that
A4:     [a',b'] >= c & c in X by A2,WAYBEL_0:def 16;
A5:   c = [c`1,c`2] by A1,MCART_1:23;
then A6:   a' >= c`1 by A4,YELLOW_3:11;
        c`1 in proj1 X by A4,A5,FUNCT_5:4;
      hence a in uparrow proj1 X by A6,WAYBEL_0:def 16;
    end;
    let b be set;
    assume b in proj2 uparrow X;
    then consider a being set such that
A7:   [a,b] in uparrow X by FUNCT_5:def 2;
A8: a in the carrier of S & b in the carrier of T by A1,A7,ZFMISC_1:106;
    then reconsider S' = S, T' = T as non empty RelStr by STRUCT_0:def 1;
    reconsider a' = a as Element of S' by A8;
    reconsider b' = b as Element of T' by A8;
    consider c being Element of [:S',T':] such that
A9:   [a',b'] >= c & c in X by A7,WAYBEL_0:def 16;
A10: c = [c`1,c`2] by A1,MCART_1:23;
then A11: b' >= c`2 by A9,YELLOW_3:11;
      c`2 in proj2 X by A9,A10,FUNCT_5:4;
    hence b in uparrow proj2 X by A11,WAYBEL_0:def 16;
  end;

theorem
  for S being RelStr, T being reflexive RelStr, X being 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:];
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    thus proj1 uparrow X c= uparrow proj1 X by Th33;
    let a be set; assume
A2:   a in uparrow proj1 X;
    then reconsider S' = S as non empty RelStr by STRUCT_0:def 1;
    reconsider a' = a as Element of S' by A2;
    consider b being Element of S' such that
A3:   b <= a' & b in proj1 X by A2,WAYBEL_0:def 16;
    consider b2 being set such that
A4:   [b,b2] in X by A3,FUNCT_5:def 1;
A5: b2 in the carrier of T by A1,A4,ZFMISC_1:106;
    then reconsider T' = T as non empty reflexive RelStr by STRUCT_0:def 1;
    reconsider b2 as Element of T' by A5;
      b2 <= b2;
    then [b,b2] <= [a',b2] by A3,YELLOW_3:11;
    then [a',b2] in uparrow X by A4,WAYBEL_0:def 16;
    hence a in proj1 uparrow X by FUNCT_5:def 1;
  end;

theorem
  for S being reflexive RelStr, T being RelStr, X being 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:];
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    thus proj2 uparrow X c= uparrow proj2 X by Th33;
    let c be set; assume
A2:   c in uparrow proj2 X;
    then reconsider T' = T as non empty RelStr by STRUCT_0:def 1;
    reconsider c' = c as Element of T' by A2;
    consider b being Element of T' such that
A3:   b <= c' & b in proj2 X by A2,WAYBEL_0:def 16;
    consider b1 being set such that
A4:   [b1,b] in X by A3,FUNCT_5:def 2;
A5: b1 in the carrier of S by A1,A4,ZFMISC_1:106;
    then reconsider S' = S as non empty reflexive RelStr by STRUCT_0:def 1;
    reconsider b1 as Element of S' by A5;
      b1 <= b1;
    then [b1,b] <= [b1,c'] by A3,YELLOW_3:11;
    then [b1,c'] in uparrow X by A4,WAYBEL_0:def 16;
    hence c in proj2 uparrow X by FUNCT_5:def 2;
  end;

theorem
  for S, T being non empty RelStr, s being Element of S, t being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    hereby
      let x be set;
      assume x in [:downarrow s,downarrow t:];
      then consider x1, x2 being set such that
A2:     x1 in downarrow s & x2 in downarrow t & x = [x1,x2]
          by ZFMISC_1:def 2;
      reconsider x1 as Element of S by A2;
      reconsider x2 as Element of T by A2;
        s >= x1 & t >= x2 by A2,WAYBEL_0:17;
      then [s,t] >= [x1,x2] by YELLOW_3:11;
      hence x in downarrow [s,t] by A2,WAYBEL_0:17;
    end;
    let x be set; assume
A3:   x in downarrow [s,t];
    then reconsider x' = x as Element of [:S,T:];
A4: x' = [x'`1,x'`2] by A1,MCART_1:23;
   [s,t] >= x' by A3,WAYBEL_0:17;
then s >= x'`1 & t >= x'`2 by A4,YELLOW_3:11;
    then x`1 in downarrow s & x`2 in downarrow t by WAYBEL_0:17;
    hence x in [:downarrow s,downarrow t:] by A4,MCART_1:11;
  end;

theorem Th37:
for S, T being non empty RelStr, x being 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:23;
    hereby
      let a be set;
      assume a in proj1 downarrow x;
      then consider b being set such that
A3:     [a,b] in downarrow x by FUNCT_5:def 1;
A4:   a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106;
      then reconsider a' = a as Element of S;
      reconsider b as Element of T by A4;
        [a',b] <= x by A3,WAYBEL_0:17;
      then a' <= x`1 by A2,YELLOW_3:11;
      hence a in downarrow x`1 by WAYBEL_0:17;
    end;
    let b be set;
    assume b in proj2 downarrow x;
    then consider a being set such that
A5:   [a,b] in downarrow x by FUNCT_5:def 2;
A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106;
    then reconsider b' = b as Element of T;
    reconsider a as Element of S by A6;
      [a,b'] <= x by A5,WAYBEL_0:17;
    then b' <= x`2 by A2,YELLOW_3:11;
    hence b in downarrow x`2 by WAYBEL_0:17;
  end;

theorem
  for S being non empty RelStr, T being non empty reflexive RelStr,
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj1 downarrow x c= downarrow x`1 by Th37;
    let a be set; assume
A2:   a in downarrow x`1;
    then reconsider a' = a as Element of S;
A3: a' <= x`1 by A2,WAYBEL_0:17;
      x`2 <= x`2;
    then [a',x`2] <= [x`1,x`2] by A3,YELLOW_3:11;
    then [a',x`2] in downarrow [x`1,x`2] by WAYBEL_0:17;
    hence a in proj1 downarrow x by A1,FUNCT_5:def 1;
  end;

theorem
  for S being non empty reflexive RelStr, T being non empty RelStr,
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj2 downarrow x c= downarrow x`2 by Th37;
    let b be set; assume
A2:   b in downarrow x`2;
    then reconsider b' = b as Element of T;
A3: b' <= x`2 by A2,WAYBEL_0:17;
      x`1 <= x`1;
    then [x`1,b'] <= [x`1,x`2] by A3,YELLOW_3:11;
    then [x`1,b'] in downarrow [x`1,x`2] by WAYBEL_0:17;
    hence b in proj2 downarrow x by A1,FUNCT_5:def 2;
  end;

theorem
  for S, T being non empty RelStr, s being Element of S, t being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    hereby
      let x be set;
      assume x in [:uparrow s,uparrow t:];
      then consider x1, x2 being set such that
A2:     x1 in uparrow s & x2 in uparrow t & x = [x1,x2]
          by ZFMISC_1:def 2;
      reconsider x1 as Element of S by A2;
      reconsider x2 as Element of T by A2;
        s <= x1 & t <= x2 by A2,WAYBEL_0:18;
      then [s,t] <= [x1,x2] by YELLOW_3:11;
      hence x in uparrow [s,t] by A2,WAYBEL_0:18;
    end;
    let x be set; assume
A3:   x in uparrow [s,t];
    then reconsider x' = x as Element of [:S,T:];
A4: x' = [x'`1,x'`2] by A1,MCART_1:23;
   [s,t] <= x' by A3,WAYBEL_0:18;
then s <= x'`1 & t <= x'`2 by A4,YELLOW_3:11;
    then x`1 in uparrow s & x`2 in uparrow t by WAYBEL_0:18;
    hence x in [:uparrow s,uparrow t:] by A4,MCART_1:11;
  end;

theorem Th41:
for S, T being non empty RelStr, x being 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:23;
    hereby
      let a be set;
      assume a in proj1 uparrow x;
      then consider b being set such that
A3:     [a,b] in uparrow x by FUNCT_5:def 1;
A4:   a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106;
      then reconsider a' = a as Element of S;
      reconsider b as Element of T by A4;
        [a',b] >= x by A3,WAYBEL_0:18;
      then a' >= x`1 by A2,YELLOW_3:11;
      hence a in uparrow x`1 by WAYBEL_0:18;
    end;
    let b be set;
    assume b in proj2 uparrow x;
    then consider a being set such that
A5:   [a,b] in uparrow x by FUNCT_5:def 2;
A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106;
    then reconsider b' = b as Element of T;
    reconsider a as Element of S by A6;
      [a,b'] >= x by A5,WAYBEL_0:18;
    then b' >= x`2 by A2,YELLOW_3:11;
    hence b in uparrow x`2 by WAYBEL_0:18;
  end;

theorem
  for S being non empty RelStr, T being non empty reflexive RelStr,
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj1 uparrow x c= uparrow x`1 by Th41;
    let a be set; assume
A2:   a in uparrow x`1;
    then reconsider a' = a as Element of S;
A3: a' >= x`1 by A2,WAYBEL_0:18;
      x`2 <= x`2;
    then [a',x`2] >= [x`1,x`2] by A3,YELLOW_3:11;
    then [a',x`2] in uparrow [x`1,x`2] by WAYBEL_0:18;
    hence a in proj1 uparrow x by A1,FUNCT_5:def 1;
  end;

theorem
  for S being non empty reflexive RelStr, T being non empty RelStr,
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj2 uparrow x c= uparrow x`2 by Th41;
    let b be set; assume
A2:   b in uparrow x`2;
    then reconsider b' = b as Element of T;
A3: b' >= x`2 by A2,WAYBEL_0:18;
      x`1 <= x`1;
    then [x`1,b'] >= [x`1,x`2] by A3,YELLOW_3:11;
    then [x`1,b'] in uparrow [x`1,x`2] by WAYBEL_0:18;
    hence b in proj2 uparrow x by A1,FUNCT_5:def 2;
  end;

theorem Th44:
for S, T being up-complete (non empty Poset),
    s being Element of S, t being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    hereby
      let x be set;
      assume x in [:waybelow s,waybelow t:];
      then consider x1, x2 being set such that
A2:     x1 in waybelow s & x2 in waybelow t & x = [x1,x2]
          by ZFMISC_1:def 2;
      reconsider x1 as Element of S by A2;
      reconsider x2 as Element of T by A2;
        s >> x1 & t >> x2 by A2,WAYBEL_3:7;
      then [s,t] >> [x1,x2] by Th19;
      hence x in waybelow [s,t] by A2,WAYBEL_3:7;
    end;
    let x be set; assume
A3:   x in waybelow [s,t];
    then reconsider x' = x as Element of [:S,T:];
A4: x' = [x'`1,x'`2] by A1,MCART_1:23;
   [s,t] >> x' by A3,WAYBEL_3:7;
    then s >> x'`1 & t >> x'`2 by A4,Th19;
    then x`1 in waybelow s & x`2 in waybelow t by WAYBEL_3:7;
    hence x in [:waybelow s,waybelow t:] by A4,MCART_1:11;
  end;

theorem Th45:
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being 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:23;
    hereby
      let a be set;
      assume a in proj1 waybelow x;
      then consider b being set such that
A3:     [a,b] in waybelow x by FUNCT_5:def 1;
A4:   a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106;
      then reconsider a' = a as Element of S;
      reconsider b as Element of T by A4;
        [a',b] << x by A3,WAYBEL_3:7;
      then a' << x`1 by A2,Th18;
      hence a in waybelow x`1 by WAYBEL_3:7;
    end;
    let b be set;
    assume b in proj2 waybelow x;
    then consider a being set such that
A5:   [a,b] in waybelow x by FUNCT_5:def 2;
A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106;
    then reconsider b' = b as Element of T;
    reconsider a as Element of S by A6;
      [a,b'] << x by A5,WAYBEL_3:7;
    then b' << x`2 by A2,Th18;
    hence b in waybelow x`2 by WAYBEL_3:7;
  end;

theorem Th46:
for S being up-complete (non empty Poset),
    T being up-complete lower-bounded (non empty Poset),
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj1 waybelow x c= waybelow x`1 by Th45;
    let a be set; assume
A2:   a in waybelow x`1;
    then reconsider a' = a as Element of S;
A3: a' << x`1 by A2,WAYBEL_3:7;
      Bottom T << x`2 by WAYBEL_3:4;
    then [a',Bottom T] << [x`1,x`2] by A3,Th19;
    then [a',Bottom T] in waybelow [x`1,x`2] by WAYBEL_3:7;
    hence a in proj1 waybelow x by A1,FUNCT_5:def 1;
  end;

theorem Th47:
for S being up-complete lower-bounded (non empty Poset),
    T being up-complete (non empty Poset),
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj2 waybelow x c= waybelow x`2 by Th45;
    let a be set; assume
A2:   a in waybelow x`2;
    then reconsider a' = a as Element of T;
A3: a' << x`2 by A2,WAYBEL_3:7;
      Bottom S << x`1 by WAYBEL_3:4;
    then [Bottom S,a'] << [x`1,x`2] by A3,Th19;
    then [Bottom S,a'] in waybelow [x`1,x`2] by WAYBEL_3:7;
    hence a in proj2 waybelow x by A1,FUNCT_5:def 2;
  end;

theorem
  for S, T being up-complete (non empty Poset),
    s being Element of S, t being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    hereby
      let x be set;
      assume x in [:wayabove s,wayabove t:];
      then consider x1, x2 being set such that
A2:     x1 in wayabove s & x2 in wayabove t & x = [x1,x2]
          by ZFMISC_1:def 2;
      reconsider x1 as Element of S by A2;
      reconsider x2 as Element of T by A2;
        s << x1 & t << x2 by A2,WAYBEL_3:8;
      then [s,t] << [x1,x2] by Th19;
      hence x in wayabove [s,t] by A2,WAYBEL_3:8;
    end;
    let x be set; assume
A3:   x in wayabove [s,t];
    then reconsider x' = x as Element of [:S,T:];
A4: x' = [x'`1,x'`2] by A1,MCART_1:23;
   [s,t] << x' by A3,WAYBEL_3:8;
then s << x'`1 & t << x'`2 by A4,Th19;
    then x`1 in wayabove s & x`2 in wayabove t by WAYBEL_3:8;
    hence x in [:wayabove s,wayabove t:] by A4,MCART_1:11;
  end;

theorem
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being 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:23;
    hereby
      let a be set;
      assume a in proj1 wayabove x;
      then consider b being set such that
A3:     [a,b] in wayabove x by FUNCT_5:def 1;
A4:   a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106;
      then reconsider a' = a as Element of S;
      reconsider b as Element of T by A4;
        [a',b] >> x by A3,WAYBEL_3:8;
      then a' >> x`1 by A2,Th18;
      hence a in wayabove x`1 by WAYBEL_3:8;
    end;
    let b be set;
    assume b in proj2 wayabove x;
    then consider a being set such that
A5:   [a,b] in wayabove x by FUNCT_5:def 2;
A6: a in the carrier of S & b in the carrier of T by A1,A5,ZFMISC_1:106;
    then reconsider b' = b as Element of T;
    reconsider a as Element of S by A6;
      [a,b'] >> x by A5,WAYBEL_3:8;
    then b' >> x`2 by A2,Th18;
    hence b in wayabove x`2 by WAYBEL_3:8;
  end;

theorem Th50:
for S, T being up-complete (non empty Poset),
    s being Element of S, t being 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;
A1: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    hereby
      let x be set;
      assume x in [:compactbelow s,compactbelow t:];
      then consider x1, x2 being set such that
A2:     x1 in compactbelow s & x2 in compactbelow t & x = [x1,x2]
          by ZFMISC_1:def 2;
      reconsider x1 as Element of S by A2;
      reconsider x2 as Element of T by A2;
        s >= x1 & t >= x2 by A2,WAYBEL_8:4;
then A3:   [s,t] >= [x1,x2] by YELLOW_3:11;
A4:   [x1,x2]`1 = x1 & [x1,x2]`2 = x2 by MCART_1:7;
        x1 is compact & x2 is compact by A2,WAYBEL_8:4;
      then [x1,x2] is compact by A4,Th23;
      hence x in compactbelow [s,t] by A2,A3,WAYBEL_8:4;
    end;
    let x be set; assume
A5:   x in compactbelow [s,t];
    then reconsider x' = x as Element of [:S,T:];
A6: x' = [x'`1,x'`2] by A1,MCART_1:23;
A7: [s,t] >= x' & x' is compact by A5,WAYBEL_8:4;
then A8: s >= x'`1 & t >= x'`2 by A6,YELLOW_3:11;
      x'`1 is compact & x'`2 is compact by A7,Th22;
    then x`1 in compactbelow s & x`2 in compactbelow t by A8,WAYBEL_8:4;
    hence x in [:compactbelow s,compactbelow t:] by A6,MCART_1:11;
  end;

theorem Th51:
for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    x being 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:23;
    hereby
      let a be set;
      assume a in proj1 compactbelow x;
      then consider b being set such that
A3:     [a,b] in compactbelow x by FUNCT_5:def 1;
A4:   a in the carrier of S & b in the carrier of T by A1,A3,ZFMISC_1:106;
      then reconsider a' = a as Element of S;
      reconsider b as Element of T by A4;
A5:   [a',b]`1 = a' & [a',b]`2 = b by MCART_1:7;
        [a',b] <= x & [a',b] is compact by A3,WAYBEL_8:4;
      then a' <= x`1 & a' is compact by A2,A5,Th22,YELLOW_3:11;
      hence a in compactbelow x`1 by WAYBEL_8:4;
    end;
    let b be set;
    assume b in proj2 compactbelow x;
    then consider a being set such that
A6:   [a,b] in compactbelow x by FUNCT_5:def 2;
A7: a in the carrier of S & b in the carrier of T by A1,A6,ZFMISC_1:106;
    then reconsider b' = b as Element of T;
    reconsider a as Element of S by A7;
A8: [a,b']`1 = a & [a,b']`2 = b' by MCART_1:7;
      [a,b'] <= x & [a,b'] is compact by A6,WAYBEL_8:4;
    then b' <= x`2 & b' is compact by A2,A8,Th22,YELLOW_3:11;
    hence b in compactbelow x`2 by WAYBEL_8:4;
  end;

theorem Th52:
for S being up-complete (non empty Poset),
    T being up-complete lower-bounded (non empty Poset),
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj1 compactbelow x c= compactbelow x`1 by Th51;
    let a be set; assume
A2:   a in compactbelow x`1;
    then reconsider a' = a as Element of S;
A3: a' <= x`1 & a' is compact by A2,WAYBEL_8:4;
      Bottom T <= x`2 by YELLOW_0:44;
then A4: [a',Bottom T] <= [x`1,x`2] by A3,YELLOW_3:11;
A5: [a',Bottom T]`1 = a' & [a',Bottom T]`2 = Bottom T by MCART_1:7;
      Bottom T is compact by WAYBEL_3:15;
    then [a',Bottom T] is compact by A3,A5,Th23;
    then [a',Bottom T] in compactbelow [x`1,x`2] by A4,WAYBEL_8:4;
    hence a in proj1 compactbelow x by A1,FUNCT_5:def 1;
  end;

theorem Th53:
for S being up-complete lower-bounded (non empty Poset),
    T being up-complete (non empty Poset),
    x being 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:];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
then A1: x = [x`1,x`2] by MCART_1:23;
    thus proj2 compactbelow x c= compactbelow x`2 by Th51;
    let a be set; assume
A2:   a in compactbelow x`2;
    then reconsider a' = a as Element of T;
A3: a' <= x`2 & a' is compact by A2,WAYBEL_8:4;
      Bottom S <= x`1 by YELLOW_0:44;
then A4: [Bottom S,a'] <= [x`1,x`2] by A3,YELLOW_3:11;
A5: [Bottom S,a']`1 = Bottom S & [Bottom S,a']`2 = a' by MCART_1:7;
      Bottom S is compact by WAYBEL_3:15;
    then [Bottom S,a'] is compact by A3,A5,Th23;
    then [Bottom S,a'] in compactbelow [x`1,x`2] by A4,WAYBEL_8:4;
    hence a in proj2 compactbelow x by A1,FUNCT_5:def 2;
  end;

definition let S be non empty reflexive RelStr;
 cluster empty -> Open 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
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being 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 being Element of [:S,T:] st x in X
       ex y being 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 being set such that
A3:     [s,t] in X by FUNCT_5:def 1;
        t in the carrier of T by A2,A3,ZFMISC_1:106;
      then reconsider t as Element of T;
      consider y being Element of [:S,T:] such that
A4:     y in X & y << [s,t] by A1,A3;
      take z = y`1;
A5:   y = [y`1,y`2] by A2,MCART_1:23;
      hence z in proj1 X by A4,FUNCT_5:def 1;
      thus z << s by A4,A5,Th18;
    end;
    let t be Element of T;
    assume t in proj2 X;
    then consider s being set such that
A6:   [s,t] in X by FUNCT_5:def 2;
      s in the carrier of S by A2,A6,ZFMISC_1:106;
    then reconsider s as Element of S;
    consider y being Element of [:S,T:] such that
A7:   y in X & y << [s,t] by A1,A6;
    take z = y`2;
A8: y = [y`1,y`2] by A2,MCART_1:23;
    hence z in proj2 X by A7,FUNCT_5:def 2;
    thus z << t by A7,A8,Th18;
  end;

theorem
  for S, T being up-complete (non empty Poset),
    X being Subset of S, Y being 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 being Element of S st x in X
       ex y being Element of S st y in X & y << x and
A2:   for x being Element of T st x in Y
       ex y being 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:23;
    then x`1 in X by A3,ZFMISC_1:106;
    then consider s being Element of S such that
A5:   s in X & s << x`1 by A1;
      x`2 in Y by A3,A4,ZFMISC_1:106;
    then consider t being Element of T such that
A6:   t in Y & t << x`2 by A2;
    reconsider t as Element of T;
    take [s,t];
    thus [s,t] in [:X,Y:] by A5,A6,ZFMISC_1:106;
    thus [s,t] << x by A4,A5,A6,Th19;
  end;

theorem
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being 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 being 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 being set such that
A3:     [sup D, t] in X by FUNCT_5:def 1;
        t in the carrier of T by A2,A3,ZFMISC_1:106;
then A4:   t is Element of T;
      then reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:5;
        ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75;
      then sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by YELLOW_3:
46
        .= [sup D, sup proj2 [:D,t':]] by FUNCT_5:11
        .= [sup D,sup t'] by FUNCT_5:11
        .= [sup D,t] by A4,YELLOW_0:39;
      then [:D,{t}:] meets X by A1,A3;
      then consider x being set such that
A5:     x in [:D,{t}:] & x in X by XBOOLE_0:3;
      thus D meets proj1 X
      proof
          now take a = x`1;
          x = [a,x`2] by A5,MCART_1:23;
        hence a in D & a in proj1 X by A5,FUNCT_5:4,ZFMISC_1:106;
        end; hence thesis by XBOOLE_0:3;
      end;
    end;
    let D be non empty directed Subset of T;
    assume sup D in proj2 X;
    then consider s being set such that
A6:   [s,sup D] in X by FUNCT_5:def 2;
      s in the carrier of S by A2,A6,ZFMISC_1:106;
then A7: s is Element of S;
    then reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5;
      ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75;
    then sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',D:]] by YELLOW_3:46
      .= [sup s', sup proj2 [:s',D:]] by FUNCT_5:11
      .= [sup s',sup D] by FUNCT_5:11
      .= [s,sup D] by A7,YELLOW_0:39;
    then [:{s},D:] meets X by A1,A6;
    then consider x being set such that
A8:   x in [:{s},D:] & x in X by XBOOLE_0:3;
      now take a = x`2;
      x = [x`1,a] by A8,MCART_1:23;
    hence a in D & a in proj2 X by A8,FUNCT_5:4,ZFMISC_1:106;
    end; hence thesis by XBOOLE_0:3;
  end;

theorem
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being upper Subset of S, Y being 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 being non empty directed Subset of S st sup D in X
       holds D meets X and
A2:   for D being 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:];
A4: proj1 D is non empty directed & proj2 D is non empty directed
     by YELLOW_3:21,22;
      ex_sup_of D,[:S,T:] by WAYBEL_0:75;
    then sup D = [sup proj1 D, sup proj2 D] by YELLOW_3:46;
    then sup proj1 D in X & sup proj2 D in Y by A3,ZFMISC_1:106;
then A5: proj1 D meets X & proj2 D meets Y by A1,A2,A4;
    then consider s being set such that
A6:   s in proj1 D & s in X by XBOOLE_0:3;
    consider t being set such that
A7:   t in proj2 D & t in Y by A5,XBOOLE_0:3;
    reconsider s as Element of S by A6;
    reconsider t as Element of T by A7;
    consider s2 being set such that
A8:  [s,s2] in D by A6,FUNCT_5:def 1;
A9: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    then s2 in the carrier of T by A8,ZFMISC_1:106;
    then reconsider s2 as Element of T;
    consider t1 being set such that
A10:  [t1,t] in D by A7,FUNCT_5:def 2;
      t1 in the carrier of S by A9,A10,ZFMISC_1:106;
    then reconsider t1 as Element of S;
    consider z being Element of [:S,T:] such that
A11:  z in D and
A12:  [s,s2] <= z & [t1,t] <= z by A8,A10,WAYBEL_0:def 1;
      now take z;
    thus z in D by A11;
A13:z = [z`1,z`2] by A9,MCART_1:23;
    then s <= z`1 & t <= z`2 by A12,YELLOW_3:11;
    then z`1 in X & z`2 in Y by A6,A7,WAYBEL_0:def 20;
    hence z in [:X,Y:] by A13,ZFMISC_1:106;
    end; hence thesis by XBOOLE_0:3;
  end;

theorem
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of S, Y being 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 being 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
        let D be non empty directed Subset of S such that
A3:       D c= X;
        consider t being set such that
A4:       t in Y by A2,XBOOLE_0:def 1;
A5:     t is Element of T by A4;
        then reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:
5;
          t' c= Y by A4,ZFMISC_1:37;
then A6:     [:D,t':] c= [:X,Y:] by A3,ZFMISC_1:119;
          ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75;
then A7:     sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by
YELLOW_3:46
          .= [sup D, sup proj2 [:D,t':]] by FUNCT_5:11
          .= [sup D,sup t'] by FUNCT_5:11
          .= [sup D,t] by A5,YELLOW_0:39;
          sup [:D,t':] in [:X,Y:] by A1,A6;
        hence sup D in X by A7,ZFMISC_1:106;
      end;
    end;
    assume
A8:   X <> {};
    let D be non empty directed Subset of T such that
A9:   D c= Y;
    consider s being set such that
A10:   s in X by A8,XBOOLE_0:def 1;
A11: s is Element of S by A10;
    then reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5;
      s' c= X by A10,ZFMISC_1:37;
then A12: [:s',D:] c= [:X,Y:] by A9,ZFMISC_1:119;
      ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75;
then A13: sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',D:]] by YELLOW_3:
46
        .= [sup s',sup proj2 [:s',D:]] by FUNCT_5:11
        .= [sup s',sup D] by FUNCT_5:11
        .= [s,sup D] by A11,YELLOW_0:39;
      sup [:s',D:] in [:X,Y:] by A1,A12;
    hence sup D in Y by A13,ZFMISC_1:106;
  end;

theorem
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of S, Y being 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 being non empty directed Subset of S st D c= X holds sup D in X and
A2:  for D being 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 D c= [:X,Y:];
then A3: proj1 D c= X & proj2 D c= Y by FUNCT_5:13;
      proj1 D is non empty directed & proj2 D is non empty directed
      by YELLOW_3:21,22;
then A4: sup proj1 D in X & sup proj2 D in Y by A1,A2,A3;
      ex_sup_of D,[:S,T:] by WAYBEL_0:75;
    then sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
    hence sup D in [:X,Y:] by A4,ZFMISC_1:106;
  end;

theorem
  for S, T being antisymmetric up-complete (non empty reflexive RelStr),
    X being Subset of [:S,T:] st X has_the_property_(S) holds
 proj1 X has_the_property_(S) & proj2 X has_the_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 being non empty directed Subset of [:S,T:] st sup D in X
      ex y being Element of [:S,T:] st y in D &
       for x being 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 being set such that
A3:     [sup D, t] in X by FUNCT_5:def 1;
        t in the carrier of T by A2,A3,ZFMISC_1:106;
      then reconsider t as Element of T;
      reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:5;
        ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75;
      then sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by YELLOW_3:
46
        .= [sup D, sup proj2 [:D,t':]] by FUNCT_5:11
        .= [sup D,sup t'] by FUNCT_5:11
        .= [sup D,t] by YELLOW_0:39;
      then consider y being Element of [:S,T:] such that
A4:    y in [:D,t':] and
A5:    for x being Element of [:S,T:] st x in [:D,t':] & x >= y holds x in X
         by A1,A3;
      take z = y`1;
A6:   y = [y`1,y`2] by A2,MCART_1:23;
      hence z in D by A4,ZFMISC_1:106;
      let x be Element of S;
      assume x in D;
then A7:   [x,t] in [:D,t':] by ZFMISC_1:129;
      assume
A8:     x >= z;
A9:   y`2 = t by A4,A6,ZFMISC_1:129;
        y`2 <= y`2;
      then [x,t] >= y by A6,A8,A9,YELLOW_3:11;
      then [x,t] in X by A5,A7;
      hence x in proj1 X by FUNCT_5:4;
    end;
    let D be non empty directed Subset of T;
    assume sup D in proj2 X;
    then consider s being set such that
A10:  [s,sup D] in X by FUNCT_5:def 2;
      s in the carrier of S by A2,A10,ZFMISC_1:106;
    then reconsider s as Element of S;
    reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5;
      ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75;
    then sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',D:]] by YELLOW_3:46
      .= [sup s', sup proj2 [:s',D:]] by FUNCT_5:11
      .= [sup s',sup D] by FUNCT_5:11
      .= [s,sup D] by YELLOW_0:39;
    then consider y being Element of [:S,T:] such that
A11:    y in [:s',D:] and
A12:    for x being Element of [:S,T:] st x in [:s',D:] & x >= y holds x in X
       by A1,A10;
    take z = y`2;
A13: y = [y`1,y`2] by A2,MCART_1:23;
    hence z in D by A11,ZFMISC_1:106;
    let x be Element of T;
    assume x in D;
then A14: [s,x] in [:s',D:] by ZFMISC_1:128;
    assume
A15:   x >= z;
A16: y`1 = s by A11,A13,ZFMISC_1:128;
      y`1 <= y`1;
    then [s,x] >= y by A13,A15,A16,YELLOW_3:11;
    then [s,x] in X by A12,A14;
    hence x in proj2 X by FUNCT_5:4;
  end;

theorem
  for S, T being up-complete (non empty Poset),
    X being Subset of S, Y being Subset of T
  st X has_the_property_(S) & Y has_the_property_(S)
 holds [:X,Y:] has_the_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 being non empty directed Subset of S st sup D in X
       ex y being Element of S st y in D &
        for x being Element of S st x in D & x >= y holds x in X and
A2:   for D being non empty directed Subset of T st sup D in Y
       ex y being Element of T st y in D &
        for x being 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:];
A4: proj1 D is non empty directed & proj2 D is non empty directed
      by YELLOW_3:21,22;
      ex_sup_of D,[:S,T:] by WAYBEL_0:75;
    then sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
then A5: sup proj1 D in X & sup proj2 D in Y by A3,ZFMISC_1:106;
    then consider s being Element of S such that
A6:  s in proj1 D and
A7:  for x being Element of S st x in proj1 D & x >= s holds x in X by A1,A4;
    consider t being Element of T such that
A8:  t in proj2 D and
A9:  for x being Element of T st x in proj2 D & x >=
 t holds x in Y by A2,A4,A5;
    consider s2 being set such that
A10:  [s,s2] in D by A6,FUNCT_5:def 1;
A11: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    then s2 in the carrier of T by A10,ZFMISC_1:106;
    then reconsider s2 as Element of T;
    consider t1 being set such that
A12:  [t1,t] in D by A8,FUNCT_5:def 2;
      t1 in the carrier of S by A11,A12,ZFMISC_1:106;
    then reconsider t1 as Element of S;
    consider z being Element of [:S,T:] such that
A13:  z in D and
A14:  [s,s2] <= z & [t1,t] <= z by A10,A12,WAYBEL_0:def 1;
    take z;
    thus z in D by A13;
    let x be Element of [:S,T:] such that
A15:  x in D;
    assume x >= z;
then A16: x`1 >= z`1 & x`2 >= z`2 by YELLOW_3:12;
A17:x = [x`1,x`2] by A11,MCART_1:23;
then A18:x`1 in proj1 D & x`2 in proj2 D by A15,FUNCT_5:4;
      z = [z`1,z`2] by A11,MCART_1:23;
    then s <= z`1 & t <= z`2 by A14,YELLOW_3:11;
    then x`1 >= s & x`2 >= t by A16,ORDERS_1:26;
    then x`1 in X & x`2 in Y by A7,A9,A18;
    hence x in [:X,Y:] by A17,ZFMISC_1:106;
  end;


begin  :: On the products of relational structures

theorem Th62:
for S, T being 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 being non empty Subset of S
        ex x being Element of S st x is_<=_than X &
         for y being Element of S st y is_<=_than X holds x >= y;
    let X be non empty Subset of T;
      X is Subset of S by A1;
    then consider x being Element of S such that
A3:   x is_<=_than X and
A4:   for y being Element of S st y is_<=_than X holds x >= y by 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 s is_<=_than X by A1,YELLOW_0:2;
    then x >= s by A4;
    hence z >= y by A1,YELLOW_0:1;
  end;

definition let S be /\-complete (non empty reflexive RelStr);
 cluster the RelStr of S -> /\-complete;
coherence by Th62;
end;

definition 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 being Element of S such that
A1:  s is_<=_than proj1 X and
A2:  for y being 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 being Element of T such that
A3:  t is_<=_than proj2 X and
A4:  for y being 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:23;
    assume y is_<=_than X;
    then y`1 is_<=_than proj1 X & y`2 is_<=_than proj2 X by A5,YELLOW_3:34;
    then s >= y`1 & t >= y`2 by A2,A4;
    hence [s,t] >= y by A5,YELLOW_3:11;
  end;
end;

theorem
  for S, T being 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 being non empty Subset of [:S,T:]
      ex x being Element of [:S,T:] st x is_<=_than X &
       for y being 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
      let X be non empty Subset of S;
      consider t being Element of T;
      consider x being Element of [:S,T:] such that
A3:     x is_<=_than [:X,{t}:] and
A4:     for y being 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:23;
      hence x`1 is_<=_than X by A3,YELLOW_3:32;
      let y be Element of S such that
A6:     y is_<=_than X;
        t <= t;
      then t is_<=_than {t} by YELLOW_0:7;
      then [y,t] is_<=_than [:X,{t}:] by A6,YELLOW_3:33;
      then x >= [y,t] by A4;
      hence x`1 >= y by A5,YELLOW_3:11;
    end;
    let X be non empty Subset of T;
    consider s being Element of S;
    consider x being Element of [:S,T:] such that
A7:   x is_<=_than [:{s},X:] and
A8:   for y being 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:23;
    hence x`2 is_<=_than X by A7,YELLOW_3:32;
    let y be Element of T such that
A10:   y is_<=_than X;
      s <= s;
    then s is_<=_than {s} by YELLOW_0:7;
    then [s,y] is_<=_than [:{s},X:] by A10,YELLOW_3:33;
    then x >= [s,y] by A8;
    hence x`2 >= y by A9,YELLOW_3:11;
  end;

definition 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 being Element of S such that
A1:   s is_a_complement_of x`1 by WAYBEL_1:def 24;
    consider t being Element of T such that
A2:   t is_a_complement_of x`2 by WAYBEL_1:def 24;
    take [s,t];
      the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    then [s,t]`1 = s & [s,t]`2 = t & x = [x`1,x`2] by MCART_1:7,23;
    hence [s,t] is_a_complement_of x by A1,A2,Th17;
  end;
end;

theorem
  for S, T being 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;
    assume
A1:   for x being Element of [:S,T:]
       ex y being Element of [:S,T:] st y is_a_complement_of x;
A2: the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
      by YELLOW_3:def 2;
    thus S is complemented
    proof
      let s be Element of S;
      consider t being Element of T;
      consider y being Element of [:S,T:] such that
A3:     y is_a_complement_of [s,t] by A1;
      take y`1;
        [s,t]`1 = s & [s,t]`2 = t & y = [y`1,y`2] by A2,MCART_1:7,23;
      hence y`1 is_a_complement_of s by A3,Th17;
    end;
    let t be Element of T;
    consider s being Element of S;
    consider y being Element of [:S,T:] such that
A4:   y is_a_complement_of [s,t] by A1;
    take y`2;
      [s,t]`1 = s & [s,t]`2 = t & y = [y`1,y`2] by A2,MCART_1:7,23;
    hence y`2 is_a_complement_of t by A4,Th17;
  end;

definition 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))`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;
      (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;
    hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\"
 z) by A1,A2,DOMAIN_1:12;
  end;
end;

theorem
  for S being with_infima with_suprema antisymmetric RelStr,
    T being 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 being Element of [:S,T:] holds
      x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z);
    let x, y, z be Element of S;
    consider t being Element of T;
      t <= t;
then A2: t "\/" t = t & t "/\" t = t by YELLOW_0:24,25;
    thus x "/\" (y "\/" z)
      = [x "/\" (y "\/" z),t]`1 by MCART_1:7
     .= ([x,t] "/\" [y "\/" z,t])`1 by A2,Th15
     .= ([x,t] "/\" ([y,t] "\/" [z,t]))`1 by A2,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 A2,Th16
     .= (x "/\" y) "\/" (x "/\" z) by MCART_1:7;
  end;

theorem
  for S being with_infima with_suprema reflexive antisymmetric RelStr,
    T being 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 being Element of [:S,T:] holds
      x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z);
    let x, y, z be Element of T;
    consider s being Element of S;
      s <= s;
then A2: s "\/" s = s & s "/\" s = s by YELLOW_0:24,25;
    thus x "/\" (y "\/" z)
      = [s,x "/\" (y "\/" z)]`2 by MCART_1:7
     .= ([s,x] "/\" [s,y "\/" z])`2 by A2,Th15
     .= ([s,x] "/\" ([s,y] "\/" [s,z]))`2 by A2,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 A2,Th16
     .= (x "/\" y) "\/" (x "/\" z) by MCART_1:7;
  end;

definition 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,22;
A2: proj2 D is non empty directed by YELLOW_3:21,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:23;
    reconsider x' = {x} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
      ex_sup_of x' "/\" D,[:S,T:] & ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A5: sup D = [sup proj1 D,sup proj2 D] by YELLOW_3:46;
      ex_sup_of x'"/\" D,[:S,T:] by WAYBEL_0:75;
then A6: sup ({x} "/\" D) = [sup proj1 ({x} "/\" D), sup proj2 ({x} "/\" D)]
      by YELLOW_3:46;
A7: (x "/\" sup D)`1 = x`1 "/\" (sup D)`1 by Th13
                  .= x`1 "/\" sup proj1 D by A5,MCART_1:7
                  .= sup ({x`1} "/\" proj1 D) by A1,WAYBEL_2:def 6
                  .= sup (proj1 {x} "/\" proj1 D) by A4,FUNCT_5:15
                  .= sup (proj1 ({x} "/\" D)) by Th24
                  .= (sup ({x} "/\" D))`1 by A6,MCART_1:7;
      (x "/\" sup D)`2 = x`2 "/\" (sup D)`2 by Th13
                  .= x`2 "/\" sup proj2 D by A5,MCART_1:7
                  .= sup ({x`2} "/\" proj2 D) by A2,WAYBEL_2:def 6
                  .= sup (proj2 {x} "/\" proj2 D) by A4,FUNCT_5:15
                  .= sup (proj2 ({x} "/\" D)) by Th24
                  .= (sup ({x} "/\" D))`2 by A6,MCART_1:7;
    hence x "/\" sup D = sup ({x} "/\" D) by A3,A7,DOMAIN_1:12;
  end;
end;

theorem
  for S, T being 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 being Element of [:S,T:],
          D being 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;
      let s be Element of S,
          D be non empty directed Subset of S;
      consider t being Element of T;
      reconsider t' = {t} as non empty directed Subset of T by WAYBEL_0:5;
        ex_sup_of [:D,t':],[:S,T:] by A1,WAYBEL_0:75;
then A3:   sup [:D,t':] = [sup proj1 [:D,t':], sup proj2 [:D,t':]] by YELLOW_3:
46;
      reconsider ST = {[s,t]} as non empty directed Subset of [:S,T:]
        by WAYBEL_0:5;
        ex_sup_of ST "/\" [:D,t':],[:S,T:] by A1,WAYBEL_0:75;
then A4:   sup ({[s,t]} "/\" [:D,t':]) = [sup proj1 ({[s,t]} "/\" [:D,t':]),
                                   sup proj2 ({[s,t]} "/\" [:D,t':])]
        by YELLOW_3:46;
      thus sup ({s} "/\" D) = sup (proj1 {[s,t]} "/\" D) by FUNCT_5:15
        .= sup (proj1 {[s,t]} "/\" proj1 [:D,t':]) by FUNCT_5:11
        .= sup proj1 ({[s,t]} "/\" [:D,t':]) by Th24
        .= (sup ({[s,t]} "/\" [:D,t':]))`1 by A4,MCART_1:7
        .= ([s,t] "/\" sup [:D,t':] )`1 by A2
        .= [s,t]`1 "/\" (sup [:D,t':])`1 by Th13
        .= s "/\" (sup [:D,t':])`1 by MCART_1:7
        .= s "/\" sup proj1 [:D,t':] by A3,MCART_1:7
        .= s "/\" sup D by FUNCT_5:11;
    end;
    thus T is up-complete by A1,WAYBEL_2:11;
    let t be Element of T,
        D be non empty directed Subset of T;
    consider s being Element of S;
    reconsider s' = {s} as non empty directed Subset of S by WAYBEL_0:5;
      ex_sup_of [:s',D:],[:S,T:] by A1,WAYBEL_0:75;
then A5: sup [:s',D:] = [sup proj1 [:s',D:], sup proj2 [:s',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 "/\" [:s',D:],[:S,T:] by A1,WAYBEL_0:75;
then A6: sup ({[s,t]} "/\" [:s',D:]) = [sup proj1 ({[s,t]} "/\" [:s',D:]),
                                 sup proj2 ({[s,t]} "/\" [:s',D:])]
      by YELLOW_3:46;
    thus sup ({t} "/\" D) = sup (proj2 {[s,t]} "/\" D) by FUNCT_5:15
      .= sup (proj2 {[s,t]} "/\" proj2 [:s',D:]) by FUNCT_5:11
      .= sup proj2 ({[s,t]} "/\" [:s',D:]) by Th24
      .= (sup ({[s,t]} "/\" [:s',D:]))`2 by A6,MCART_1:7
      .= ([s,t] "/\" sup [:s',D:] )`2 by A2
      .= [s,t]`2 "/\" (sup [:s',D:])`2 by Th13
      .= t "/\" (sup [:s',D:])`2 by MCART_1:7
      .= t "/\" sup proj2 [:s',D:] by A5,MCART_1:7
      .= t "/\" sup D by FUNCT_5:11;
  end;

definition 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)`1 = sup proj1 waybelow x by MCART_1:7
      .= sup waybelow x`1 by Th46
      .= x`1 by WAYBEL_3:def 5;
      (sup waybelow x)`2 = sup proj2 waybelow x by A2,MCART_1:7
      .= sup waybelow x`2 by Th47
      .= x`2 by WAYBEL_3:def 5;
    hence x = sup waybelow x by A1,A3,DOMAIN_1:12;
  end;
end;

definition let S, T be continuous /\-complete (non empty Poset);
 cluster [:S,T:] -> continuous;
coherence
  proof
    thus for x being Element of [:S,T:] holds
     waybelow x is non empty directed;
    thus [:S,T:] is up-complete satisfying_axiom_of_approximation;
  end;
end;

theorem
  for S, T being 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 being Element of [:S,T:] holds waybelow x is non empty directed and
A2:  [:S,T:] is up-complete satisfying_axiom_of_approximation;
A3: 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;
    hereby
      hereby
        let s be Element of S;
        consider t being Element of T;
A4:     [:waybelow s,waybelow t:] = waybelow [s,t] by Th44;
A5:     proj1 [:waybelow s,waybelow t:] = waybelow s by FUNCT_5:11;
          waybelow [s,t] is directed by A1;
        hence waybelow s is non empty directed by A4,A5,YELLOW_3:22;
      end;
      thus S is up-complete;
      thus S is satisfying_axiom_of_approximation
      proof
        let s be Element of S;
        consider t being Element of T;
          waybelow [s,t] is directed by A1;
        then ex_sup_of waybelow [s,t], [:S,T:] by WAYBEL_0:75;
then A6:     sup waybelow [s,t] =
         [sup proj1 waybelow [s,t],sup proj2 waybelow [s,t]] by Th5;
        thus s = [s,t]`1 by MCART_1:7
              .= (sup waybelow [s,t])`1 by A2,WAYBEL_3:def 5
              .= sup proj1 waybelow [s,t] by A6,MCART_1:7
              .= sup waybelow [s,t]`1 by Th46
              .= sup waybelow s by MCART_1:7;
      end;
    end;
    hereby
      let t be Element of T;
      consider s being Element of S;
A7:   [:waybelow s,waybelow t:] = waybelow [s,t] by Th44;
A8:   proj2 [:waybelow s,waybelow t:] = waybelow t by FUNCT_5:11;
        waybelow [s,t] is directed by A1;
      hence waybelow t is non empty directed by A7,A8,YELLOW_3:22;
    end;
    thus T is up-complete;
    let t be Element of T;
    consider s being Element of S;
      ex_sup_of waybelow [s,t], [:S,T:] by A3;
then A9: sup waybelow [s,t] = [sup proj1 waybelow [s,t],sup proj2 waybelow [s,t
]]
      by Th5;
    thus t = [s,t]`2 by MCART_1:7
          .= (sup waybelow [s,t])`2 by A2,WAYBEL_3:def 5
          .= sup proj2 waybelow [s,t] by A9,MCART_1:7
          .= sup waybelow [s,t]`2 by Th47
          .= sup waybelow t by MCART_1:7;
  end;

definition 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)`1 = sup proj1 compactbelow x by MCART_1:7
      .= sup compactbelow x`1 by Th52
      .= x`1 by WAYBEL_8:def 3;
      (sup compactbelow x)`2 = sup proj2 compactbelow x by A2,MCART_1:7
      .= sup compactbelow x`2 by Th53
      .= x`2 by WAYBEL_8:def 3;
    hence x = sup compactbelow x by A1,A3,DOMAIN_1:12;
  end;
end;

definition let S, T be complete algebraic lower-bounded sup-Semilattice;
 cluster [:S,T:] -> algebraic;
coherence
  proof
    thus for x being Element of [:S,T:] holds
     compactbelow x is non empty directed;
    thus [:S,T:] is up-complete satisfying_axiom_K;
  end;
end;

theorem Th69:
for S, T being 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 being 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
        let s be Element of S;
        consider t being Element of T;
A4:     [:compactbelow s,compactbelow t:] = compactbelow [s,t] by A3,Th50;
A5:     proj1 [:compactbelow s,compactbelow t:] = compactbelow s by FUNCT_5:11;
          compactbelow [s,t] is directed by A1;
        hence compactbelow s is non empty directed by A4,A5,YELLOW_3:22;
      end;
      thus S is up-complete by A2,WAYBEL_2:11;
      thus S is satisfying_axiom_K
      proof
        let s be Element of S;
        consider t being 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 A6:     sup compactbelow [s,t] =
          [sup proj1 compactbelow [s,t],sup proj2 compactbelow [s,t]] by Th5;
        thus s = [s,t]`1 by MCART_1:7
              .= (sup compactbelow [s,t])`1 by A2,WAYBEL_8:def 3
              .= sup proj1 compactbelow [s,t] by A6,MCART_1:7
              .= sup compactbelow [s,t]`1 by A3,Th52
              .= sup compactbelow s by MCART_1:7;
      end;
    end;
    hereby
      let t be Element of T;
      consider s being Element of S;
A7:   [:compactbelow s,compactbelow t:] = compactbelow [s,t] by A3,Th50;
A8:   proj2 [:compactbelow s,compactbelow t:] = compactbelow t by FUNCT_5:11;
        compactbelow [s,t] is directed by A1;
      hence compactbelow t is non empty directed by A7,A8,YELLOW_3:22;
    end;
    thus T is up-complete by A2,WAYBEL_2:11;
    let t be Element of T;
    consider s being 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 A9: sup compactbelow [s,t] =
      [sup proj1 compactbelow [s,t],sup proj2 compactbelow [s,t]] by Th5;
    thus t = [s,t]`2 by MCART_1:7
          .= (sup compactbelow [s,t])`2 by A2,WAYBEL_8:def 3
          .= sup proj2 compactbelow [s,t] by A9,MCART_1:7
          .= sup compactbelow [s,t]`2 by A3,Th53
          .= sup compactbelow t by MCART_1:7;
  end;

definition let S, T be arithmetic lower-bounded LATTICE;
 cluster [:S,T:] -> arithmetic;
coherence
  proof
    thus [:S,T:] is algebraic;
    set C = CompactSublatt [:S,T:];
    let x, y be Element of [:S,T:] such that
A1:   x in the carrier of C & y in the carrier of C & ex_inf_of {x,y},[:S,T:];
A2: CompactSublatt S is meet-inheriting & CompactSublatt T is meet-inheriting
      by WAYBEL_8:def 5;
A3: ex_inf_of {x`1,y`1},S & ex_inf_of {x`2,y`2},T by YELLOW_0:21;
      x is compact & y is compact by A1,WAYBEL_8:def 1;
    then x`1 is compact & y`1 is compact & x`2 is compact & y`2 is compact by
Th22;
    then x`1 in the carrier of CompactSublatt S &
     y`1 in the carrier of CompactSublatt S &
      x`2 in the carrier of CompactSublatt T &
       y`2 in the carrier of CompactSublatt T by WAYBEL_8:def 1;
    then inf {x`1,y`1} in the carrier of CompactSublatt S &
     inf {x`2,y`2} in the carrier of CompactSublatt T
      by A2,A3,YELLOW_0:def 16;
    then x`1 "/\" y`1 in the carrier of CompactSublatt S &
     x`2 "/\" y`2 in the carrier of CompactSublatt T
      by YELLOW_0:40;
    then x`1 "/\" y`1 is compact & x`2 "/\" y`2 is compact by WAYBEL_8:def 1;
    then (x "/\" y)`1 is compact & (x "/\" y)`2 is compact by Th13;
    then x "/\" y is compact by Th23;
    then inf {x,y} is compact by YELLOW_0:40;
    hence inf {x,y} in the carrier of C by WAYBEL_8:def 1;
  end;
end;

theorem
  for S, T being 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;
      [:S,T:] is up-complete by A1,WAYBEL_8:def 4;
then A3: S is up-complete & T is up-complete by 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 &
        y in the carrier of CompactSublatt S and ex_inf_of {x,y},S;
A5:   ex_inf_of {[x,Bottom T], [y,Bottom T]}, [:S,T:] by YELLOW_0:21;
A6:   Bottom T is compact by WAYBEL_3:15;
A7:   [x,Bottom T]`1 = x & [y,Bottom T]`1 = y & [x,Bottom T]`2 = Bottom T & [y,
Bottom T]`2 = Bottom T
        by MCART_1:7;
        x is compact & y is compact by A4,WAYBEL_8:def 1;
      then [x,Bottom T] is compact & [y,Bottom
T] is compact by A3,A6,A7,Th23;
      then [x,Bottom T] in the carrier of CompactSublatt [:S,T:] &
       [y,Bottom
T] in the carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1;
      then inf {[x,Bottom T], [y,Bottom T]} in the carrier of CompactSublatt
[:S,T:]
        by A2,A5,YELLOW_0:def 16;
then A8:   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 by MCART_1:7
         .= x "/\" y by MCART_1:7;
      then x "/\" y is compact by A3,A8,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
A9:   x in the carrier of CompactSublatt T &
      y in the carrier of CompactSublatt T and ex_inf_of {x,y},T;
A10: ex_inf_of {[Bottom S,x], [Bottom S,y]}, [:S,T:] by YELLOW_0:21;
A11: Bottom S is compact by WAYBEL_3:15;
A12: [Bottom S,x]`2 = x & [Bottom S,y]`2 = y & [Bottom S,x]`1 = Bottom S & [
Bottom S,y]`1 = Bottom S
    by MCART_1:7;
      x is compact & y is compact by A9,WAYBEL_8:def 1;
    then [Bottom S,x] is compact & [Bottom
S,y] is compact by A3,A11,A12,Th23;
    then [Bottom S,x] in the carrier of CompactSublatt [:S,T:] &
     [Bottom
S,y] in the carrier of CompactSublatt [:S,T:] by WAYBEL_8:def 1;
    then inf {[Bottom S,x], [Bottom S,y]} in the carrier of CompactSublatt [:S
,T:]
      by A2,A10,YELLOW_0:def 16;
then A13: 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 by MCART_1:7
       .= x "/\" y by MCART_1:7;
    then x "/\" y is compact by A3,A13,Th22;
    then inf {x,y} is compact by YELLOW_0:40;
    hence inf {x,y} in the carrier of CompactSublatt T by WAYBEL_8:def 1;
  end;


Back to top