:: YELLOW10 semantic presentation

begin

registration
let S, T be non empty upper-bounded RelStr ;
cluster[:S,T:] ->  upper-bounded ;
coherence
 [:S,T:] is upper-bounded
proof
A1: the carrier of T c= the carrier of T ;
consider t being Element of T such that
A2: t is_>=_than the carrier of T by YELLOW_0:def_5;
consider s being Element of S such that
A3: s is_>=_than the carrier of S by YELLOW_0:def_5;
take  [s,t] ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of [:S,T:] is_<=_than [s,t]
 ( the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] & the carrier of S c= the carrier of S ) by YELLOW_3:def_2;
hence  the carrier of [:S,T:] is_<=_than [s,t] by A3, A2, A1, YELLOW_3:30; ::_thesis: verum
end;
end;

registration
let S, T be non empty lower-bounded RelStr ;
cluster[:S,T:] ->  lower-bounded ;
coherence
 [:S,T:] is lower-bounded
proof
A1: the carrier of T c= the carrier of T ;
consider t being Element of T such that
A2: t is_<=_than the carrier of T by YELLOW_0:def_4;
consider s being Element of S such that
A3: s is_<=_than the carrier of S by YELLOW_0:def_4;
take  [s,t] ; :: according to YELLOW_0:def_4 ::_thesis: [s,t] is_<=_than the carrier of [:S,T:]
 ( the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] & the carrier of S c= the carrier of S ) by YELLOW_3:def_2;
hence  [s,t] is_<=_than the carrier of [:S,T:] by A3, A2, A1, YELLOW_3:33; ::_thesis: verum
end;
end;

theorem :: YELLOW10:1
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 ; ::_thesis: ( [:S,T:] is upper-bounded implies ( S is upper-bounded & T is upper-bounded ) )
given x being Element of [:S,T:] such that A1: x is_>=_than the carrier of [:S,T:] ; :: according to YELLOW_0:def_5 ::_thesis: ( S is upper-bounded & T is upper-bounded )
 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 and
A3: t in the carrier of T and
A4: x = [s,t] by ZFMISC_1:def_2;
reconsider t = t as Element of T by A3;
reconsider s = s as Element of S by A2;
A5: ( the carrier of S c= the carrier of S & the carrier of T c= the carrier of T ) ;
A6: [s,t] is_>=_than [: the carrier of S, the carrier of T:] by A1, A4, YELLOW_3:def_2;
thus  S is upper-bounded ::_thesis: T is upper-bounded
proof
take  s ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of S is_<=_than s
thus  the carrier of S is_<=_than s by A5, A6, YELLOW_3:29; ::_thesis: verum
end;
take  t ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of T is_<=_than t
thus  the carrier of T is_<=_than t by A5, A6, YELLOW_3:29; ::_thesis: verum
end;

theorem :: YELLOW10:2
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 ; ::_thesis: ( [:S,T:] is lower-bounded implies ( S is lower-bounded & T is lower-bounded ) )
given x being Element of [:S,T:] such that A1: x is_<=_than the carrier of [:S,T:] ; :: according to YELLOW_0:def_4 ::_thesis: ( S is lower-bounded & T is lower-bounded )
 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 and
A3: t in the carrier of T and
A4: x = [s,t] by ZFMISC_1:def_2;
reconsider t = t as Element of T by A3;
reconsider s = s as Element of S by A2;
A5: ( the carrier of S c= the carrier of S & the carrier of T c= the carrier of T ) ;
A6: [s,t] is_<=_than [: the carrier of S, the carrier of T:] by A1, A4, YELLOW_3:def_2;
thus  S is lower-bounded ::_thesis: T is lower-bounded
proof
take  s ; :: according to YELLOW_0:def_4 ::_thesis: s is_<=_than the carrier of S
thus  s is_<=_than the carrier of S by A5, A6, YELLOW_3:32; ::_thesis: verum
end;
take  t ; :: according to YELLOW_0:def_4 ::_thesis: t is_<=_than the carrier of T
thus  t is_<=_than the carrier of T by A5, A6, YELLOW_3:32; ::_thesis: verum
end;

theorem Th3: :: YELLOW10:3
for S, T being non empty antisymmetric upper-bounded RelStr holds Top [:S,T:] = [(Top S),(Top T)]
proof
let S, T be non empty antisymmetric upper-bounded RelStr ; ::_thesis: Top [:S,T:] = [(Top S),(Top T)]
A1: 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:]; ::_thesis: ( {} is_>=_than a implies a <= [(Top S),(Top T)] )
assume  {} is_>=_than a ; ::_thesis: a <= [(Top S),(Top 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 and
A3: t in the carrier of T and
A4: a = [s,t] by ZFMISC_1:def_2;
reconsider t = t as Element of T by A3;
reconsider s = s as Element of S by A2;
 ( s <= Top S & t <= Top T ) by YELLOW_0:45;
hence  a <= [(Top S),(Top T)] by A4, YELLOW_3:11; ::_thesis: verum
end;
 ( ex_inf_of {} ,[:S,T:] & {} is_>=_than [(Top S),(Top T)] ) by YELLOW_0:6, YELLOW_0:43;
hence  Top [:S,T:] = [(Top S),(Top T)] by A1, YELLOW_0:def_10; ::_thesis: verum
end;

theorem Th4: :: YELLOW10:4
for S, T being non empty antisymmetric lower-bounded RelStr holds Bottom [:S,T:] = [(Bottom S),(Bottom T)]
proof
let S, T be non empty antisymmetric lower-bounded RelStr ; ::_thesis: Bottom [:S,T:] = [(Bottom S),(Bottom T)]
A1: 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:]; ::_thesis: ( {} is_<=_than a implies [(Bottom S),(Bottom T)] <= a )
assume  {} is_<=_than a ; ::_thesis: [(Bottom S),(Bottom T)] <= 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
A2: s in the carrier of S and
A3: t in the carrier of T and
A4: a = [s,t] by ZFMISC_1:def_2;
reconsider t = t as Element of T by A3;
reconsider s = s as Element of S by A2;
 ( Bottom S <= s & Bottom T <= t ) by YELLOW_0:44;
hence  [(Bottom S),(Bottom T)] <= a by A4, YELLOW_3:11; ::_thesis: verum
end;
 ( ex_sup_of {} ,[:S,T:] & {} is_<=_than [(Bottom S),(Bottom T)] ) by YELLOW_0:6, YELLOW_0:42;
hence  Bottom [:S,T:] = [(Bottom S),(Bottom T)] by A1, YELLOW_0:def_9; ::_thesis: verum
end;

theorem Th5: :: YELLOW10:5
for S, T being non empty antisymmetric lower-bounded RelStr
for 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 non empty antisymmetric lower-bounded RelStr ; ::_thesis: for 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))]
let D be Subset of [:S,T:]; ::_thesis: ( ( [:S,T:] is complete or ex_sup_of D,[:S,T:] ) implies sup D = [(sup (proj1 D)),(sup (proj2 D))] )
assume A1: ( [:S,T:] is complete or ex_sup_of D,[:S,T:] ) ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
percases ( D <> {} or D = {} ) ;
suppose D <> {} ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
hence  sup D = [(sup (proj1 D)),(sup (proj2 D))] by A1, YELLOW_3:46; ::_thesis: verum
end;
supposeA2: D = {} ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
then A3: sup (proj2 D) = Bottom T ;
 ( sup D = Bottom [:S,T:] & sup (proj1 D) = Bottom S ) by A2;
hence  sup D = [(sup (proj1 D)),(sup (proj2 D))] by A3, Th4; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW10:6
for S, T being non empty antisymmetric upper-bounded RelStr
for 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 non empty antisymmetric upper-bounded RelStr ; ::_thesis: for 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))]
let D be Subset of [:S,T:]; ::_thesis: ( ( [:S,T:] is complete or ex_inf_of D,[:S,T:] ) implies inf D = [(inf (proj1 D)),(inf (proj2 D))] )
assume A1: ( [:S,T:] is complete or ex_inf_of D,[:S,T:] ) ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
percases ( D <> {} or D = {} ) ;
suppose D <> {} ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
hence  inf D = [(inf (proj1 D)),(inf (proj2 D))] by A1, YELLOW_3:47; ::_thesis: verum
end;
supposeA2: D = {} ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
then A3: inf (proj2 D) = Top T ;
 ( inf D = Top [:S,T:] & inf (proj1 D) = Top S ) by A2;
hence  inf D = [(inf (proj1 D)),(inf (proj2 D))] by A3, Th3; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW10:7
for S, T being non empty RelStr
for 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 ; ::_thesis: for 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)} ) )
let x, y be Element of [:S,T:]; ::_thesis: ( x is_<=_than {y} iff ( x `1 is_<=_than {(y `1)} & x `2 is_<=_than {(y `2)} ) )
thus  ( x is_<=_than {y} implies ( x `1 is_<=_than {(y `1)} & x `2 is_<=_than {(y `2)} ) ) ::_thesis: ( x `1 is_<=_than {(y `1)} & x `2 is_<=_than {(y `2)} implies x is_<=_than {y} )
proof
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
 y = [(y `1),(y `2)] by A1, MCART_1:21;
then A3: [(y `1),(y `2)] in {y} by TARSKI:def_1;
assume  for b being Element of [:S,T:] st b in {y} holds
x <= b ; :: according to LATTICE3:def_8 ::_thesis: ( x `1 is_<=_than {(y `1)} & x `2 is_<=_than {(y `2)} )
then A4: x <= [(y `1),(y `2)] by A3;
hereby  :: according to LATTICE3:def_8 ::_thesis: x `2 is_<=_than {(y `2)}
let b be Element of S; ::_thesis: ( b in {(y `1)} implies x `1 <= b )
assume  b in {(y `1)} ; ::_thesis: x `1 <= b
then  b = y `1 by TARSKI:def_1;
hence  x `1 <= b by A4, A2, YELLOW_3:11; ::_thesis: verum
end;
let b be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not b in {(y `2)} or x `2 <= b )
assume  b in {(y `2)} ; ::_thesis: x `2 <= b
then  b = y `2 by TARSKI:def_1;
hence  x `2 <= b by A4, A2, YELLOW_3:11; ::_thesis: verum
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 ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than {y}
let b be Element of [:S,T:]; :: according to LATTICE3:def_8 ::_thesis: ( not b in {y} or x <= b )
assume  b in {y} ; ::_thesis: x <= b
then A7: b = y by TARSKI:def_1;
then  b `2 in {(y `2)} by TARSKI:def_1;
then A8: x `2 <= b `2 by A6;
 b `1 in {(y `1)} by A7, TARSKI:def_1;
then  x `1 <= b `1 by A5;
hence  x <= b by A8, YELLOW_3:12; ::_thesis: verum
end;

theorem :: YELLOW10:8
for S, T being non empty RelStr
for 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 ; ::_thesis: for 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)} ) )
let x, y, z be Element of [:S,T:]; ::_thesis: ( x is_<=_than {y,z} iff ( x `1 is_<=_than {(y `1),(z `1)} & x `2 is_<=_than {(y `2),(z `2)} ) )
thus  ( x is_<=_than {y,z} implies ( x `1 is_<=_than {(y `1),(z `1)} & x `2 is_<=_than {(y `2),(z `2)} ) ) ::_thesis: ( x `1 is_<=_than {(y `1),(z `1)} & x `2 is_<=_than {(y `2),(z `2)} implies x is_<=_than {y,z} )
proof
assume A1: for b being Element of [:S,T:] st b in {y,z} holds
x <= b ; :: according to LATTICE3:def_8 ::_thesis: ( x `1 is_<=_than {(y `1),(z `1)} & x `2 is_<=_than {(y `2),(z `2)} )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  y = [(y `1),(y `2)] by MCART_1:21;
then  [(y `1),(y `2)] in {y,z} by TARSKI:def_2;
then A3: x <= [(y `1),(y `2)] by A1;
 z = [(z `1),(z `2)] by A2, MCART_1:21;
then  [(z `1),(z `2)] in {y,z} by TARSKI:def_2;
then A4: x <= [(z `1),(z `2)] by A1;
A5: x = [(x `1),(x `2)] by A2, MCART_1:21;
hereby  :: according to LATTICE3:def_8 ::_thesis: x `2 is_<=_than {(y `2),(z `2)}
let b be Element of S; ::_thesis: ( b in {(y `1),(z `1)} implies x `1 <= b )
assume  b in {(y `1),(z `1)} ; ::_thesis: x `1 <= b
then  ( b = y `1 or b = z `1 ) by TARSKI:def_2;
hence  x `1 <= b by A3, A4, A5, YELLOW_3:11; ::_thesis: verum
end;
let b be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not b in {(y `2),(z `2)} or x `2 <= b )
assume  b in {(y `2),(z `2)} ; ::_thesis: x `2 <= b
then  ( b = y `2 or b = z `2 ) by TARSKI:def_2;
hence  x `2 <= b by A3, A4, A5, YELLOW_3:11; ::_thesis: verum
end;
assume that
A6: for b being Element of S st b in {(y `1),(z `1)} holds
x `1 <= b and
A7: for b being Element of T st b in {(y `2),(z `2)} holds
x `2 <= b ; :: according to LATTICE3:def_8 ::_thesis: x is_<=_than {y,z}
let b be Element of [:S,T:]; :: according to LATTICE3:def_8 ::_thesis: ( not b in {y,z} or x <= b )
assume  b in {y,z} ; ::_thesis: x <= b
then A8: ( b = y or b = z ) by TARSKI:def_2;
then  b `2 in {(y `2),(z `2)} by TARSKI:def_2;
then A9: x `2 <= b `2 by A7;
 b `1 in {(y `1),(z `1)} by A8, TARSKI:def_2;
then  x `1 <= b `1 by A6;
hence  x <= b by A9, YELLOW_3:12; ::_thesis: verum
end;

theorem :: YELLOW10:9
for S, T being non empty RelStr
for 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 ; ::_thesis: for 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)} ) )
let x, y be Element of [:S,T:]; ::_thesis: ( x is_>=_than {y} iff ( x `1 is_>=_than {(y `1)} & x `2 is_>=_than {(y `2)} ) )
thus  ( x is_>=_than {y} implies ( x `1 is_>=_than {(y `1)} & x `2 is_>=_than {(y `2)} ) ) ::_thesis: ( x `1 is_>=_than {(y `1)} & x `2 is_>=_than {(y `2)} implies x is_>=_than {y} )
proof
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
 y = [(y `1),(y `2)] by A1, MCART_1:21;
then A3: [(y `1),(y `2)] in {y} by TARSKI:def_1;
assume  for b being Element of [:S,T:] st b in {y} holds
x >= b ; :: according to LATTICE3:def_9 ::_thesis: ( x `1 is_>=_than {(y `1)} & x `2 is_>=_than {(y `2)} )
then A4: x >= [(y `1),(y `2)] by A3;
hereby  :: according to LATTICE3:def_9 ::_thesis: x `2 is_>=_than {(y `2)}
let b be Element of S; ::_thesis: ( b in {(y `1)} implies x `1 >= b )
assume  b in {(y `1)} ; ::_thesis: x `1 >= b
then  b = y `1 by TARSKI:def_1;
hence  x `1 >= b by A4, A2, YELLOW_3:11; ::_thesis: verum
end;
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in {(y `2)} or b <= x `2 )
assume  b in {(y `2)} ; ::_thesis: b <= x `2
then  b = y `2 by TARSKI:def_1;
hence  b <= x `2 by A4, A2, YELLOW_3:11; ::_thesis: verum
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 ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than {y}
let b be Element of [:S,T:]; :: according to LATTICE3:def_9 ::_thesis: ( not b in {y} or b <= x )
assume  b in {y} ; ::_thesis: b <= x
then A7: b = y by TARSKI:def_1;
then  b `2 in {(y `2)} by TARSKI:def_1;
then A8: x `2 >= b `2 by A6;
 b `1 in {(y `1)} by A7, TARSKI:def_1;
then  x `1 >= b `1 by A5;
hence  b <= x by A8, YELLOW_3:12; ::_thesis: verum
end;

theorem :: YELLOW10:10
for S, T being non empty RelStr
for 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 ; ::_thesis: for 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)} ) )
let x, y, z be Element of [:S,T:]; ::_thesis: ( x is_>=_than {y,z} iff ( x `1 is_>=_than {(y `1),(z `1)} & x `2 is_>=_than {(y `2),(z `2)} ) )
thus  ( x is_>=_than {y,z} implies ( x `1 is_>=_than {(y `1),(z `1)} & x `2 is_>=_than {(y `2),(z `2)} ) ) ::_thesis: ( x `1 is_>=_than {(y `1),(z `1)} & x `2 is_>=_than {(y `2),(z `2)} implies x is_>=_than {y,z} )
proof
assume A1: for b being Element of [:S,T:] st b in {y,z} holds
x >= b ; :: according to LATTICE3:def_9 ::_thesis: ( x `1 is_>=_than {(y `1),(z `1)} & x `2 is_>=_than {(y `2),(z `2)} )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  y = [(y `1),(y `2)] by MCART_1:21;
then  [(y `1),(y `2)] in {y,z} by TARSKI:def_2;
then A3: x >= [(y `1),(y `2)] by A1;
 z = [(z `1),(z `2)] by A2, MCART_1:21;
then  [(z `1),(z `2)] in {y,z} by TARSKI:def_2;
then A4: x >= [(z `1),(z `2)] by A1;
A5: x = [(x `1),(x `2)] by A2, MCART_1:21;
hereby  :: according to LATTICE3:def_9 ::_thesis: x `2 is_>=_than {(y `2),(z `2)}
let b be Element of S; ::_thesis: ( b in {(y `1),(z `1)} implies x `1 >= b )
assume  b in {(y `1),(z `1)} ; ::_thesis: x `1 >= b
then  ( b = y `1 or b = z `1 ) by TARSKI:def_2;
hence  x `1 >= b by A3, A4, A5, YELLOW_3:11; ::_thesis: verum
end;
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in {(y `2),(z `2)} or b <= x `2 )
assume  b in {(y `2),(z `2)} ; ::_thesis: b <= x `2
then  ( b = y `2 or b = z `2 ) by TARSKI:def_2;
hence  b <= x `2 by A3, A4, A5, YELLOW_3:11; ::_thesis: verum
end;
assume that
A6: for b being Element of S st b in {(y `1),(z `1)} holds
x `1 >= b and
A7: for b being Element of T st b in {(y `2),(z `2)} holds
x `2 >= b ; :: according to LATTICE3:def_9 ::_thesis: x is_>=_than {y,z}
let b be Element of [:S,T:]; :: according to LATTICE3:def_9 ::_thesis: ( not b in {y,z} or b <= x )
assume  b in {y,z} ; ::_thesis: b <= x
then A8: ( b = y or b = z ) by TARSKI:def_2;
then  b `2 in {(y `2),(z `2)} by TARSKI:def_2;
then A9: x `2 >= b `2 by A7;
 b `1 in {(y `1),(z `1)} by A8, TARSKI:def_2;
then  x `1 >= b `1 by A6;
hence  b <= x by A9, YELLOW_3:12; ::_thesis: verum
end;

theorem :: YELLOW10:11
for S, T being non empty antisymmetric RelStr
for 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 ; ::_thesis: for 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 ) )
let x, y be Element of [:S,T:]; ::_thesis: ( ex_inf_of {x,y},[:S,T:] iff ( ex_inf_of {(x `1),(y `1)},S & ex_inf_of {(x `2),(y `2)},T ) )
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;
then  ( proj1 {x,y} = {(x `1),(y `1)} & proj2 {x,y} = {(x `2),(y `2)} ) by FUNCT_5:13;
hence  ( ex_inf_of {x,y},[:S,T:] iff ( ex_inf_of {(x `1),(y `1)},S & ex_inf_of {(x `2),(y `2)},T ) ) by YELLOW_3:42; ::_thesis: verum
end;

theorem :: YELLOW10:12
for S, T being non empty antisymmetric RelStr
for 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 ; ::_thesis: for 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 ) )
let x, y be Element of [:S,T:]; ::_thesis: ( ex_sup_of {x,y},[:S,T:] iff ( ex_sup_of {(x `1),(y `1)},S & ex_sup_of {(x `2),(y `2)},T ) )
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;
then  ( proj1 {x,y} = {(x `1),(y `1)} & proj2 {x,y} = {(x `2),(y `2)} ) by FUNCT_5:13;
hence  ( ex_sup_of {x,y},[:S,T:] iff ( ex_sup_of {(x `1),(y `1)},S & ex_sup_of {(x `2),(y `2)},T ) ) by YELLOW_3:41; ::_thesis: verum
end;

theorem Th13: :: YELLOW10:13
for S, T being antisymmetric with_infima RelStr
for 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 antisymmetric with_infima RelStr ; ::_thesis: for x, y being Element of [:S,T:] holds
( (x "/\" y) `1 = (x `1) "/\" (y `1) & (x "/\" y) `2 = (x `2) "/\" (y `2) )
let x, y be Element of [:S,T:]; ::_thesis: ( (x "/\" y) `1 = (x `1) "/\" (y `1) & (x "/\" y) `2 = (x `2) "/\" (y `2) )
set a = (x "/\" y) `1 ;
set b = (x "/\" y) `2 ;
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
A3: y = [(y `1),(y `2)] by A1, MCART_1:21;
A4: for d being Element of S st d <= x `1 & d <= y `1 holds
(x "/\" y) `1 >= d
proof
set t = (x `2) "/\" (y `2);
let d be Element of S; ::_thesis: ( d <= x `1 & d <= y `1 implies (x "/\" y) `1 >= d )
assume that
A5: d <= x `1 and
A6: d <= y `1 ; ::_thesis: (x "/\" y) `1 >= d
 (x `2) "/\" (y `2) <= y `2 by YELLOW_0:23;
then A7: [d,((x `2) "/\" (y `2))] <= y by A3, A6, YELLOW_3:11;
 (x `2) "/\" (y `2) <= x `2 by YELLOW_0:23;
then  [d,((x `2) "/\" (y `2))] <= x by A2, A5, YELLOW_3:11;
then A8: x "/\" y >= [d,((x `2) "/\" (y `2))] by A7, YELLOW_0:23;
 [d,((x `2) "/\" (y `2))] `1 = d ;
hence  (x "/\" y) `1 >= d by A8, YELLOW_3:12; ::_thesis: verum
end;
A9: for d being Element of T st d <= x `2 & d <= y `2 holds
(x "/\" y) `2 >= d
proof
set s = (x `1) "/\" (y `1);
let d be Element of T; ::_thesis: ( d <= x `2 & d <= y `2 implies (x "/\" y) `2 >= d )
assume that
A10: d <= x `2 and
A11: d <= y `2 ; ::_thesis: (x "/\" y) `2 >= d
 (x `1) "/\" (y `1) <= y `1 by YELLOW_0:23;
then A12: [((x `1) "/\" (y `1)),d] <= y by A3, A11, YELLOW_3:11;
 (x `1) "/\" (y `1) <= x `1 by YELLOW_0:23;
then  [((x `1) "/\" (y `1)),d] <= x by A2, A10, YELLOW_3:11;
then A13: x "/\" y >= [((x `1) "/\" (y `1)),d] by A12, YELLOW_0:23;
 [((x `1) "/\" (y `1)),d] `2 = d ;
hence  (x "/\" y) `2 >= d by A13, YELLOW_3:12; ::_thesis: verum
end;
 x "/\" y <= y by YELLOW_0:23;
then A14: ( (x "/\" y) `1 <= y `1 & (x "/\" y) `2 <= y `2 ) by YELLOW_3:12;
 x "/\" y <= x by YELLOW_0:23;
then  ( (x "/\" y) `1 <= x `1 & (x "/\" y) `2 <= x `2 ) by YELLOW_3:12;
hence  ( (x "/\" y) `1 = (x `1) "/\" (y `1) & (x "/\" y) `2 = (x `2) "/\" (y `2) ) by A14, A4, A9, YELLOW_0:19; ::_thesis: verum
end;

theorem Th14: :: YELLOW10:14
for S, T being antisymmetric with_suprema RelStr
for 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 antisymmetric with_suprema RelStr ; ::_thesis: for x, y being Element of [:S,T:] holds
( (x "\/" y) `1 = (x `1) "\/" (y `1) & (x "\/" y) `2 = (x `2) "\/" (y `2) )
let x, y be Element of [:S,T:]; ::_thesis: ( (x "\/" y) `1 = (x `1) "\/" (y `1) & (x "\/" y) `2 = (x `2) "\/" (y `2) )
set a = (x "\/" y) `1 ;
set b = (x "\/" y) `2 ;
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
A3: y = [(y `1),(y `2)] by A1, MCART_1:21;
A4: for d being Element of S st d >= x `1 & d >= y `1 holds
(x "\/" y) `1 <= d
proof
set t = (x `2) "\/" (y `2);
let d be Element of S; ::_thesis: ( d >= x `1 & d >= y `1 implies (x "\/" y) `1 <= d )
assume that
A5: d >= x `1 and
A6: d >= y `1 ; ::_thesis: (x "\/" y) `1 <= d
 (x `2) "\/" (y `2) >= y `2 by YELLOW_0:22;
then A7: [d,((x `2) "\/" (y `2))] >= y by A3, A6, YELLOW_3:11;
 (x `2) "\/" (y `2) >= x `2 by YELLOW_0:22;
then  [d,((x `2) "\/" (y `2))] >= x by A2, A5, YELLOW_3:11;
then A8: x "\/" y <= [d,((x `2) "\/" (y `2))] by A7, YELLOW_0:22;
 [d,((x `2) "\/" (y `2))] `1 = d ;
hence  (x "\/" y) `1 <= d by A8, YELLOW_3:12; ::_thesis: verum
end;
A9: for d being Element of T st d >= x `2 & d >= y `2 holds
(x "\/" y) `2 <= d
proof
set s = (x `1) "\/" (y `1);
let d be Element of T; ::_thesis: ( d >= x `2 & d >= y `2 implies (x "\/" y) `2 <= d )
assume that
A10: d >= x `2 and
A11: d >= y `2 ; ::_thesis: (x "\/" y) `2 <= d
 (x `1) "\/" (y `1) >= y `1 by YELLOW_0:22;
then A12: [((x `1) "\/" (y `1)),d] >= y by A3, A11, YELLOW_3:11;
 (x `1) "\/" (y `1) >= x `1 by YELLOW_0:22;
then  [((x `1) "\/" (y `1)),d] >= x by A2, A10, YELLOW_3:11;
then A13: x "\/" y <= [((x `1) "\/" (y `1)),d] by A12, YELLOW_0:22;
 [((x `1) "\/" (y `1)),d] `2 = d ;
hence  (x "\/" y) `2 <= d by A13, YELLOW_3:12; ::_thesis: verum
end;
 x "\/" y >= y by YELLOW_0:22;
then A14: ( (x "\/" y) `1 >= y `1 & (x "\/" y) `2 >= y `2 ) by YELLOW_3:12;
 x "\/" y >= x by YELLOW_0:22;
then  ( (x "\/" y) `1 >= x `1 & (x "\/" y) `2 >= x `2 ) by YELLOW_3:12;
hence  ( (x "\/" y) `1 = (x `1) "\/" (y `1) & (x "\/" y) `2 = (x `2) "\/" (y `2) ) by A14, A4, A9, YELLOW_0:18; ::_thesis: verum
end;

theorem Th15: :: YELLOW10:15
for S, T being antisymmetric with_infima RelStr
for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]
proof
let S, T be antisymmetric with_infima RelStr ; ::_thesis: for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]
let x1, y1 be Element of S; ::_thesis: for x2, y2 being Element of T holds [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]
let x2, y2 be Element of T; ::_thesis: [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2]
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
A2: ([x1,x2] "/\" [y1,y2]) `2 = ([x1,x2] `2) "/\" ([y1,y2] `2) by Th13
.= x2 "/\" ([y1,y2] `2)
.= x2 "/\" y2
.= [(x1 "/\" y1),(x2 "/\" y2)] `2 ;
([x1,x2] "/\" [y1,y2]) `1 = ([x1,x2] `1) "/\" ([y1,y2] `1) by Th13
.= x1 "/\" ([y1,y2] `1)
.= x1 "/\" y1
.= [(x1 "/\" y1),(x2 "/\" y2)] `1 ;
hence  [(x1 "/\" y1),(x2 "/\" y2)] = [x1,x2] "/\" [y1,y2] by A1, A2, DOMAIN_1:2; ::_thesis: verum
end;

theorem Th16: :: YELLOW10:16
for S, T being antisymmetric with_suprema RelStr
for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
proof
let S, T be antisymmetric with_suprema RelStr ; ::_thesis: for x1, y1 being Element of S
for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
let x1, y1 be Element of S; ::_thesis: for x2, y2 being Element of T holds [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
let x2, y2 be Element of T; ::_thesis: [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2]
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
A2: ([x1,x2] "\/" [y1,y2]) `2 = ([x1,x2] `2) "\/" ([y1,y2] `2) by Th14
.= x2 "\/" ([y1,y2] `2)
.= x2 "\/" y2
.= [(x1 "\/" y1),(x2 "\/" y2)] `2 ;
([x1,x2] "\/" [y1,y2]) `1 = ([x1,x2] `1) "\/" ([y1,y2] `1) by Th14
.= x1 "\/" ([y1,y2] `1)
.= x1 "\/" y1
.= [(x1 "\/" y1),(x2 "\/" y2)] `1 ;
hence  [(x1 "\/" y1),(x2 "\/" y2)] = [x1,x2] "\/" [y1,y2] by A1, A2, DOMAIN_1:2; ::_thesis: verum
end;

definition
let S be antisymmetric with_suprema with_infima RelStr ;
let x, y be Element of S;
:: original: is_a_complement_of
redefine predy is_a_complement_of x;
symmetry
 for y, x being Element of S st R54(S,b2,b1) holds
R54(S,b1,b2)
proof
let a, b be Element of S; ::_thesis: ( R54(S,b,a) implies R54(S,a,b) )
assume  a is_a_complement_of b ; ::_thesis: R54(S,a,b)
hence  ( a "\/" b = Top S & a "/\" b = Bottom S ) by WAYBEL_1:def_23; :: according to WAYBEL_1:def_23 ::_thesis: verum
end;
end;

theorem Th17: :: YELLOW10:17
for S, T being antisymmetric bounded with_suprema with_infima RelStr
for 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 antisymmetric bounded with_suprema with_infima RelStr ; ::_thesis: for 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 ) )
let x, y be Element of [:S,T:]; ::_thesis: ( x is_a_complement_of y iff ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 ) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
hereby  ::_thesis: ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 implies x is_a_complement_of y )
assume A2: x is_a_complement_of y ; ::_thesis: ( x `1 is_a_complement_of y `1 & x `2 is_a_complement_of y `2 )
A3: (y `1) "/\" (x `1) = (y "/\" x) `1 by Th13
.= (Bottom [:S,T:]) `1 by A2, WAYBEL_1:def_23
.= [(Bottom S),(Bottom T)] `1 by Th4
.= Bottom S ;
(y `1) "\/" (x `1) = (y "\/" x) `1 by Th14
.= (Top [:S,T:]) `1 by A2, WAYBEL_1:def_23
.= [(Top S),(Top T)] `1 by Th3
.= Top S ;
hence  x `1 is_a_complement_of y `1 by A3, WAYBEL_1:def_23; ::_thesis: x `2 is_a_complement_of y `2
A4: (y `2) "/\" (x `2) = (y "/\" x) `2 by Th13
.= (Bottom [:S,T:]) `2 by A2, WAYBEL_1:def_23
.= [(Bottom S),(Bottom T)] `2 by Th4
.= Bottom T ;
(y `2) "\/" (x `2) = (y "\/" x) `2 by Th14
.= (Top [:S,T:]) `2 by A2, WAYBEL_1:def_23
.= [(Top S),(Top T)] `2 by Th3
.= Top T ;
hence  x `2 is_a_complement_of y `2 by A4, WAYBEL_1:def_23; ::_thesis: verum
end;
assume that
A5: (y `1) "\/" (x `1) = Top S and
A6: (y `1) "/\" (x `1) = Bottom S and
A7: (y `2) "\/" (x `2) = Top T and
A8: (y `2) "/\" (x `2) = Bottom T ; :: according to WAYBEL_1:def_23 ::_thesis: x is_a_complement_of y
A9: (y "\/" x) `2 = (y `2) "\/" (x `2) by Th14
.= [(Top S),(Top T)] `2 by A7 ;
(y "\/" x) `1 = (y `1) "\/" (x `1) by Th14
.= [(Top S),(Top T)] `1 by A5 ;
hence y "\/" x = [(Top S),(Top T)] by A1, A9, DOMAIN_1:2
.= Top [:S,T:] by Th3 ;
:: according to WAYBEL_1:def_23 ::_thesis: y "/\" x = Bottom [:S,T:]
A10: (y "/\" x) `2 = (y `2) "/\" (x `2) by Th13
.= [(Bottom S),(Bottom T)] `2 by A8 ;
(y "/\" x) `1 = (y `1) "/\" (x `1) by Th13
.= [(Bottom S),(Bottom T)] `1 by A6 ;
hence y "/\" x = [(Bottom S),(Bottom T)] by A1, A10, DOMAIN_1:2
.= Bottom [:S,T:] by Th4 ;
::_thesis: verum
end;

theorem Th18: :: YELLOW10:18
for S, T being non empty reflexive antisymmetric up-complete RelStr
for a, c being Element of S
for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )
proof
let S, T be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for a, c being Element of S
for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )
let a, c be Element of S; ::_thesis: for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )
let b, d be Element of T; ::_thesis: ( [a,b] << [c,d] implies ( a << c & b << d ) )
assume A1: for D being non empty directed Subset of [:S,T:] st [c,d] <= sup D holds
ex e being Element of [:S,T:] st
( e in D & [a,b] <= e ) ; :: according to WAYBEL_3:def_1 ::_thesis: ( a << c & b << d )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
thus  a << c ::_thesis: b << d
proof
reconsider d9 = {d} as non empty directed Subset of T by WAYBEL_0:5;
let D be non empty directed Subset of S; :: according to WAYBEL_3:def_1 ::_thesis: ( not c <= "\/" (D,S) or ex b1 being M2( the carrier of S) st
( b1 in D & a <= b1 ) )
assume A3: c <= sup D ; ::_thesis: ex b1 being M2( the carrier of S) st
( b1 in D & a <= b1 )
A4: d <= sup d9 by YELLOW_0:39;
 ( ex_sup_of D,S & ex_sup_of d9,T ) by WAYBEL_0:75;
then  sup [:D,d9:] = [(sup D),(sup d9)] by YELLOW_3:43;
then  [c,d] <= sup [:D,d9:] by A3, A4, YELLOW_3:11;
then consider e being Element of [:S,T:] such that
A5: e in [:D,d9:] and
A6: [a,b] <= e by A1;
take  e `1 ; ::_thesis: ( e `1 in D & a <= e `1 )
thus  e `1 in D by A5, MCART_1:10; ::_thesis: a <= e `1
 e = [(e `1),(e `2)] by A2, MCART_1:21;
hence  a <= e `1 by A6, YELLOW_3:11; ::_thesis: verum
end;
let D be non empty directed Subset of T; :: according to WAYBEL_3:def_1 ::_thesis: ( not d <= "\/" (D,T) or ex b1 being M2( the carrier of T) st
( b1 in D & b <= b1 ) )
assume A7: d <= sup D ; ::_thesis: ex b1 being M2( the carrier of T) st
( b1 in D & b <= b1 )
reconsider c9 = {c} as non empty directed Subset of S by WAYBEL_0:5;
A8: c <= sup c9 by YELLOW_0:39;
 ( ex_sup_of c9,S & ex_sup_of D,T ) by WAYBEL_0:75;
then  sup [:c9,D:] = [(sup c9),(sup D)] by YELLOW_3:43;
then  [c,d] <= sup [:c9,D:] by A7, A8, YELLOW_3:11;
then consider e being Element of [:S,T:] such that
A9: e in [:c9,D:] and
A10: [a,b] <= e by A1;
take  e `2 ; ::_thesis: ( e `2 in D & b <= e `2 )
thus  e `2 in D by A9, MCART_1:10; ::_thesis: b <= e `2
 e = [(e `1),(e `2)] by A2, MCART_1:21;
hence  b <= e `2 by A10, YELLOW_3:11; ::_thesis: verum
end;

theorem Th19: :: YELLOW10:19
for S, T being non empty up-complete Poset
for a, c being Element of S
for b, d being Element of T holds
( [a,b] << [c,d] iff ( a << c & b << d ) )
proof
let S, T be non empty up-complete Poset; ::_thesis: for a, c being Element of S
for b, d being Element of T holds
( [a,b] << [c,d] iff ( a << c & b << d ) )
let a, c be Element of S; ::_thesis: for b, d being Element of T holds
( [a,b] << [c,d] iff ( a << c & b << d ) )
let b, d be Element of T; ::_thesis: ( [a,b] << [c,d] iff ( a << c & b << d ) )
thus  ( [a,b] << [c,d] implies ( a << c & b << d ) ) by Th18; ::_thesis: ( a << c & b << d implies [a,b] << [c,d] )
assume A1: for D being non empty directed Subset of S st c <= sup D holds
ex e being Element of S st
( e in D & a <= e ) ; :: according to WAYBEL_3:def_1 ::_thesis: ( not b << d or [a,b] << [c,d] )
assume A2: for D being non empty directed Subset of T st d <= sup D holds
ex e being Element of T st
( e in D & b <= e ) ; :: according to WAYBEL_3:def_1 ::_thesis: [a,b] << [c,d]
let D be non empty directed Subset of [:S,T:]; :: according to WAYBEL_3:def_1 ::_thesis: ( not [c,d] <= "\/" (D,[:S,T:]) or ex b1 being M2( the carrier of [:S,T:]) st
( b1 in D & [a,b] <= b1 ) )
assume A3: [c,d] <= sup D ; ::_thesis: ex b1 being M2( the carrier of [:S,T:]) st
( b1 in D & [a,b] <= b1 )
 ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A4: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
then  ( not proj1 D is empty & proj1 D is directed & c <= sup (proj1 D) ) by A3, YELLOW_3:11, YELLOW_3:21, YELLOW_3:22;
then consider e being Element of S such that
A5: e in proj1 D and
A6: a <= e by A1;
consider e2 being set  such that
A7: [e,e2] in D by A5, XTUPLE_0:def_12;
 ( not proj2 D is empty & proj2 D is directed & d <= sup (proj2 D) ) by A3, A4, YELLOW_3:11, YELLOW_3:21, YELLOW_3:22;
then consider f being Element of T such that
A8: f in proj2 D and
A9: b <= f by A2;
consider f1 being set  such that
A10: [f1,f] in D by A8, XTUPLE_0:def_13;
A11: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then reconsider e2 = e2 as Element of T by A7, ZFMISC_1:87;
reconsider f1 = f1 as Element of S by A11, A10, ZFMISC_1:87;
consider ef being Element of [:S,T:] such that
A12: ef in D and
A13: ( [e,e2] <= ef & [f1,f] <= ef ) by A7, A10, WAYBEL_0:def_1;
A14: ef = [(ef `1),(ef `2)] by A11, MCART_1:21;
then  ( e <= ef `1 & f <= ef `2 ) by A13, YELLOW_3:11;
then A15: [e,f] <= ef by A14, YELLOW_3:11;
take  ef ; ::_thesis: ( ef in D & [a,b] <= ef )
thus  ef in D by A12; ::_thesis: [a,b] <= ef
 [a,b] <= [e,f] by A6, A9, YELLOW_3:11;
hence  [a,b] <= ef by A15, ORDERS_2:3; ::_thesis: verum
end;

theorem Th20: :: YELLOW10:20
for S, T being non empty reflexive antisymmetric up-complete RelStr
for x, y being Element of [:S,T:] st x << y holds
( x `1 << y `1 & x `2 << y `2 )
proof
let S, T be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for x, y being Element of [:S,T:] st x << y holds
( x `1 << y `1 & x `2 << y `2 )
let x, y be Element of [:S,T:]; ::_thesis: ( x << y implies ( x `1 << y `1 & x `2 << y `2 ) )
assume A1: x << y ; ::_thesis: ( x `1 << y `1 & x `2 << y `2 )
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;
hence  ( x `1 << y `1 & x `2 << y `2 ) by A1, Th18; ::_thesis: verum
end;

theorem Th21: :: YELLOW10:21
for S, T being non empty up-complete Poset
for x, y being Element of [:S,T:] holds
( x << y iff ( x `1 << y `1 & x `2 << y `2 ) )
proof
let S, T be non empty up-complete Poset; ::_thesis: for x, y being Element of [:S,T:] holds
( x << y iff ( x `1 << y `1 & x `2 << y `2 ) )
let x, y be Element of [:S,T:]; ::_thesis: ( x << y iff ( x `1 << y `1 & x `2 << y `2 ) )
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by MCART_1:21;
hence  ( x << y iff ( x `1 << y `1 & x `2 << y `2 ) ) by Th19; ::_thesis: verum
end;

theorem Th22: :: YELLOW10:22
for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] st x is compact holds
( x `1 is compact & x `2 is compact )
proof
let S, T be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for x being Element of [:S,T:] st x is compact holds
( x `1 is compact & x `2 is compact )
let x be Element of [:S,T:]; ::_thesis: ( x is compact implies ( x `1 is compact & x `2 is compact ) )
assume A1: x << x ; :: according to WAYBEL_3:def_2 ::_thesis: ( x `1 is compact & x `2 is compact )
hence  x `1 << x `1 by Th20; :: according to WAYBEL_3:def_2 ::_thesis: x `2 is compact
thus  x `2 << x `2 by A1, Th20; :: according to WAYBEL_3:def_2 ::_thesis: verum
end;

theorem Th23: :: YELLOW10:23
for S, T being non empty up-complete Poset
for x being Element of [:S,T:] st x `1 is compact & x `2 is compact holds
x is compact
proof
let S, T be non empty up-complete Poset; ::_thesis: for x being Element of [:S,T:] st x `1 is compact & x `2 is compact holds
x is compact
let x be Element of [:S,T:]; ::_thesis: ( x `1 is compact & x `2 is compact implies x is compact )
assume  ( x `1 << x `1 & x `2 << x `2 ) ; :: according to WAYBEL_3:def_2 ::_thesis: x is compact
hence  x << x by Th21; :: according to WAYBEL_3:def_2 ::_thesis: verum
end;

begin

theorem Th24: :: YELLOW10:24
for S, T being antisymmetric with_infima RelStr
for 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 antisymmetric with_infima RelStr ; ::_thesis: for X, Y being Subset of [:S,T:] holds
( proj1 (X "/\" Y) = (proj1 X) "/\" (proj1 Y) & proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y) )
let X, Y be Subset of [:S,T:]; ::_thesis: ( proj1 (X "/\" Y) = (proj1 X) "/\" (proj1 Y) & proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y) )
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  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: proj2 (X "/\" Y) = (proj2 X) "/\" (proj2 Y)
hereby  ::_thesis: for a being set st a in (proj1 X) "/\" (proj1 Y) holds
a in proj1 (X "/\" Y)
let a be set ; ::_thesis: ( a in proj1 (X "/\" Y) implies a in (proj1 X) "/\" (proj1 Y) )
assume  a in proj1 (X "/\" Y) ; ::_thesis: a in (proj1 X) "/\" (proj1 Y)
then consider b being set  such that
A4: [a,b] in X "/\" Y by XTUPLE_0:def_12;
consider x, y being Element of [:S,T:] such that
A5: [a,b] = x "/\" y and
A6: x in X and
A7: y in Y by A2, A4;
 x = [(x `1),(x `2)] by A1, MCART_1:21;
then A8: x `1 in proj1 X by A6, XTUPLE_0:def_12;
 y = [(y `1),(y `2)] by A1, MCART_1:21;
then A9: y `1 in proj1 Y by A7, XTUPLE_0:def_12;
a = [a,b] `1
.= (x `1) "/\" (y `1) by A5, Th13 ;
hence  a in (proj1 X) "/\" (proj1 Y) by A8, A9, YELLOW_4:37; ::_thesis: verum
end;
let a be set ; ::_thesis: ( a in (proj1 X) "/\" (proj1 Y) implies a in proj1 (X "/\" Y) )
assume  a in (proj1 X) "/\" (proj1 Y) ; ::_thesis: a in proj1 (X "/\" Y)
then consider x, y being Element of S such that
A10: a = x "/\" y and
A11: x in proj1 X and
A12: y in proj1 Y by A3;
consider x2 being set  such that
A13: [x,x2] in X by A11, XTUPLE_0:def_12;
consider y2 being set  such that
A14: [y,y2] in Y by A12, XTUPLE_0:def_12;
reconsider x2 = x2, y2 = y2 as Element of T by A1, A13, A14, ZFMISC_1:87;
 [x,x2] "/\" [y,y2] = [a,(x2 "/\" y2)] by A10, Th15;
then  [a,(x2 "/\" y2)] in X "/\" Y by A13, A14, YELLOW_4:37;
hence  a in proj1 (X "/\" Y) by XTUPLE_0:def_12; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (proj2 X) "/\" (proj2 Y) c= proj2 (X "/\" Y)
let b be set ; ::_thesis: ( b in proj2 (X "/\" Y) implies b in (proj2 X) "/\" (proj2 Y) )
assume  b in proj2 (X "/\" Y) ; ::_thesis: b in (proj2 X) "/\" (proj2 Y)
then consider a being set  such that
A15: [a,b] in X "/\" Y by XTUPLE_0:def_13;
consider x, y being Element of [:S,T:] such that
A16: [a,b] = x "/\" y and
A17: x in X and
A18: y in Y by A2, A15;
 x = [(x `1),(x `2)] by A1, MCART_1:21;
then A19: x `2 in proj2 X by A17, XTUPLE_0:def_13;
 y = [(y `1),(y `2)] by A1, MCART_1:21;
then A20: y `2 in proj2 Y by A18, XTUPLE_0:def_13;
b = [a,b] `2
.= (x `2) "/\" (y `2) by A16, Th13 ;
hence  b in (proj2 X) "/\" (proj2 Y) by A19, A20, YELLOW_4:37; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (proj2 X) "/\" (proj2 Y) or b in proj2 (X "/\" Y) )
A21: (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;
assume  b in (proj2 X) "/\" (proj2 Y) ; ::_thesis: b in proj2 (X "/\" Y)
then consider x, y being Element of T such that
A22: b = x "/\" y and
A23: x in proj2 X and
A24: y in proj2 Y by A21;
consider x1 being set  such that
A25: [x1,x] in X by A23, XTUPLE_0:def_13;
consider y1 being set  such that
A26: [y1,y] in Y by A24, XTUPLE_0:def_13;
reconsider x1 = x1, y1 = y1 as Element of S by A1, A25, A26, ZFMISC_1:87;
 [x1,x] "/\" [y1,y] = [(x1 "/\" y1),b] by A22, Th15;
then  [(x1 "/\" y1),b] in X "/\" Y by A25, A26, YELLOW_4:37;
hence  b in proj2 (X "/\" Y) by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: YELLOW10:25
for S, T being antisymmetric with_suprema RelStr
for 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 antisymmetric with_suprema RelStr ; ::_thesis: for X, Y being Subset of [:S,T:] holds
( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )
let X, Y be Subset of [:S,T:]; ::_thesis: ( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )
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  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y)
hereby  ::_thesis: for a being set st a in (proj1 X) "\/" (proj1 Y) holds
a in proj1 (X "\/" Y)
let a be set ; ::_thesis: ( a in proj1 (X "\/" Y) implies a in (proj1 X) "\/" (proj1 Y) )
assume  a in proj1 (X "\/" Y) ; ::_thesis: a in (proj1 X) "\/" (proj1 Y)
then consider b being set  such that
A4: [a,b] in X "\/" Y by XTUPLE_0:def_12;
consider x, y being Element of [:S,T:] such that
A5: [a,b] = x "\/" y and
A6: x in X and
A7: y in Y by A2, A4;
 x = [(x `1),(x `2)] by A1, MCART_1:21;
then A8: x `1 in proj1 X by A6, XTUPLE_0:def_12;
 y = [(y `1),(y `2)] by A1, MCART_1:21;
then A9: y `1 in proj1 Y by A7, XTUPLE_0:def_12;
a = [a,b] `1
.= (x `1) "\/" (y `1) by A5, Th14 ;
hence  a in (proj1 X) "\/" (proj1 Y) by A8, A9, YELLOW_4:10; ::_thesis: verum
end;
let a be set ; ::_thesis: ( a in (proj1 X) "\/" (proj1 Y) implies a in proj1 (X "\/" Y) )
assume  a in (proj1 X) "\/" (proj1 Y) ; ::_thesis: a in proj1 (X "\/" Y)
then consider x, y being Element of S such that
A10: a = x "\/" y and
A11: x in proj1 X and
A12: y in proj1 Y by A3;
consider x2 being set  such that
A13: [x,x2] in X by A11, XTUPLE_0:def_12;
consider y2 being set  such that
A14: [y,y2] in Y by A12, XTUPLE_0:def_12;
reconsider x2 = x2, y2 = y2 as Element of T by A1, A13, A14, ZFMISC_1:87;
 [x,x2] "\/" [y,y2] = [a,(x2 "\/" y2)] by A10, Th16;
then  [a,(x2 "\/" y2)] in X "\/" Y by A13, A14, YELLOW_4:10;
hence  a in proj1 (X "\/" Y) by XTUPLE_0:def_12; ::_thesis: verum
end;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (proj2 X) "\/" (proj2 Y) c= proj2 (X "\/" Y)
let b be set ; ::_thesis: ( b in proj2 (X "\/" Y) implies b in (proj2 X) "\/" (proj2 Y) )
assume  b in proj2 (X "\/" Y) ; ::_thesis: b in (proj2 X) "\/" (proj2 Y)
then consider a being set  such that
A15: [a,b] in X "\/" Y by XTUPLE_0:def_13;
consider x, y being Element of [:S,T:] such that
A16: [a,b] = x "\/" y and
A17: x in X and
A18: y in Y by A2, A15;
 x = [(x `1),(x `2)] by A1, MCART_1:21;
then A19: x `2 in proj2 X by A17, XTUPLE_0:def_13;
 y = [(y `1),(y `2)] by A1, MCART_1:21;
then A20: y `2 in proj2 Y by A18, XTUPLE_0:def_13;
b = [a,b] `2
.= (x `2) "\/" (y `2) by A16, Th14 ;
hence  b in (proj2 X) "\/" (proj2 Y) by A19, A20, YELLOW_4:10; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (proj2 X) "\/" (proj2 Y) or b in proj2 (X "\/" Y) )
A21: (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;
assume  b in (proj2 X) "\/" (proj2 Y) ; ::_thesis: b in proj2 (X "\/" Y)
then consider x, y being Element of T such that
A22: b = x "\/" y and
A23: x in proj2 X and
A24: y in proj2 Y by A21;
consider x1 being set  such that
A25: [x1,x] in X by A23, XTUPLE_0:def_13;
consider y1 being set  such that
A26: [y1,y] in Y by A24, XTUPLE_0:def_13;
reconsider x1 = x1, y1 = y1 as Element of S by A1, A25, A26, ZFMISC_1:87;
 [x1,x] "\/" [y1,y] = [(x1 "\/" y1),b] by A22, Th16;
then  [(x1 "\/" y1),b] in X "\/" Y by A25, A26, YELLOW_4:10;
hence  b in proj2 (X "\/" Y) by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: YELLOW10:26
for S, T being RelStr
for X being Subset of [:S,T:] holds downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
proof
let S, T be RelStr ; ::_thesis: for X being Subset of [:S,T:] holds downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
let X be Subset of [:S,T:]; ::_thesis: downarrow X c= [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow X or x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):] )
assume A1: x in downarrow X ; ::_thesis: x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):]
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ex a, b being set st
( a in the carrier of S & b in the carrier of T & x = [a,b] ) by A1, ZFMISC_1:def_2;
then reconsider S9 = S, T9 = T as non empty RelStr ;
reconsider x9 = x as Element of [:S9,T9:] by A1;
consider y being Element of [:S9,T9:] such that
A3: y >= x9 and
A4: y in X by A1, WAYBEL_0:def_15;
A5: y `1 >= x9 `1 by A3, YELLOW_3:12;
A6: y = [(y `1),(y `2)] by A2, MCART_1:21;
then  y `1 in proj1 X by A4, XTUPLE_0:def_12;
then A7: x `1 in downarrow (proj1 X) by A5, WAYBEL_0:def_15;
A8: y `2 >= x9 `2 by A3, YELLOW_3:12;
 y `2 in proj2 X by A4, A6, XTUPLE_0:def_13;
then A9: x `2 in downarrow (proj2 X) by A8, WAYBEL_0:def_15;
 x9 = [(x9 `1),(x9 `2)] by A2, MCART_1:21;
hence  x in [:(downarrow (proj1 X)),(downarrow (proj2 X)):] by A7, A9, MCART_1:11; ::_thesis: verum
end;

theorem :: YELLOW10:27
for S, T being RelStr
for X being Subset of S
for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]
proof
let S, T be RelStr ; ::_thesis: for X being Subset of S
for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]
let X be Subset of S; ::_thesis: for Y being Subset of T holds [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]
let Y be Subset of T; ::_thesis: [:(downarrow X),(downarrow Y):] = downarrow [:X,Y:]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: downarrow [:X,Y:] c= [:(downarrow X),(downarrow Y):]
let x be set ; ::_thesis: ( x in [:(downarrow X),(downarrow Y):] implies x in downarrow [:X,Y:] )
assume  x in [:(downarrow X),(downarrow Y):] ; ::_thesis: x in downarrow [:X,Y:]
then consider x1, x2 being set  such that
A1: x1 in downarrow X and
A2: x2 in downarrow Y and
A3: x = [x1,x2] by ZFMISC_1:def_2;
reconsider S9 = S, T9 = T as non empty RelStr by A1, A2;
reconsider x1 = x1 as Element of S9 by A1;
consider y1 being Element of S9 such that
A4: ( y1 >= x1 & y1 in X ) by A1, WAYBEL_0:def_15;
reconsider x2 = x2 as Element of T9 by A2;
consider y2 being Element of T9 such that
A5: ( y2 >= x2 & y2 in Y ) by A2, WAYBEL_0:def_15;
 ( [y1,y2] in [:X,Y:] & [y1,y2] >= [x1,x2] ) by A4, A5, YELLOW_3:11, ZFMISC_1:87;
hence  x in downarrow [:X,Y:] by A3, WAYBEL_0:def_15; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow [:X,Y:] or x in [:(downarrow X),(downarrow Y):] )
assume A6: x in downarrow [:X,Y:] ; ::_thesis: x in [:(downarrow X),(downarrow Y):]
A7: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ex a, b being set st
( a in the carrier of S & b in the carrier of T & x = [a,b] ) by A6, ZFMISC_1:def_2;
then reconsider S9 = S, T9 = T as non empty RelStr ;
reconsider x9 = x as Element of [:S9,T9:] by A6;
consider y being Element of [:S9,T9:] such that
A8: ( y >= x9 & y in [:X,Y:] ) by A6, WAYBEL_0:def_15;
 ( y `2 >= x9 `2 & y `2 in Y ) by A8, MCART_1:10, YELLOW_3:12;
then A9: x `2 in downarrow Y by WAYBEL_0:def_15;
 ( y `1 >= x9 `1 & y `1 in X ) by A8, MCART_1:10, YELLOW_3:12;
then A10: x `1 in downarrow X by WAYBEL_0:def_15;
 x9 = [(x9 `1),(x9 `2)] by A7, MCART_1:21;
hence  x in [:(downarrow X),(downarrow Y):] by A10, A9, MCART_1:11; ::_thesis: verum
end;

theorem Th28: :: YELLOW10:28
for S, T being RelStr
for 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 ; ::_thesis: for X being Subset of [:S,T:] holds
( proj1 (downarrow X) c= downarrow (proj1 X) & proj2 (downarrow X) c= downarrow (proj2 X) )
let X be Subset of [:S,T:]; ::_thesis: ( proj1 (downarrow X) c= downarrow (proj1 X) & proj2 (downarrow X) c= downarrow (proj2 X) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
hereby  :: according to TARSKI:def_3 ::_thesis: proj2 (downarrow X) c= downarrow (proj2 X)
let a be set ; ::_thesis: ( a in proj1 (downarrow X) implies a in downarrow (proj1 X) )
assume  a in proj1 (downarrow X) ; ::_thesis: a in downarrow (proj1 X)
then consider b being set  such that
A2: [a,b] in downarrow X by XTUPLE_0:def_12;
reconsider S9 = S, T9 = T as non empty RelStr by A1, A2, ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1, A2, ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1, A2, ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A3: ( [a9,b9] <= c & c in X ) by A2, WAYBEL_0:def_15;
 c = [(c `1),(c `2)] by A1, MCART_1:21;
then  ( a9 <= c `1 & c `1 in proj1 X ) by A3, XTUPLE_0:def_12, YELLOW_3:11;
hence  a in downarrow (proj1 X) by WAYBEL_0:def_15; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in proj2 (downarrow X) or b in downarrow (proj2 X) )
assume  b in proj2 (downarrow X) ; ::_thesis: b in downarrow (proj2 X)
then consider a being set  such that
A4: [a,b] in downarrow X by XTUPLE_0:def_13;
reconsider S9 = S, T9 = T as non empty RelStr by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1, A4, ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1, A4, ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A5: ( [a9,b9] <= c & c in X ) by A4, WAYBEL_0:def_15;
 c = [(c `1),(c `2)] by A1, MCART_1:21;
then  ( b9 <= c `2 & c `2 in proj2 X ) by A5, XTUPLE_0:def_13, YELLOW_3:11;
hence  b in downarrow (proj2 X) by WAYBEL_0:def_15; ::_thesis: verum
end;

theorem :: YELLOW10:29
for S being RelStr
for T being reflexive RelStr
for X being Subset of [:S,T:] holds proj1 (downarrow X) = downarrow (proj1 X)
proof
let S be RelStr ; ::_thesis: for T being reflexive RelStr
for X being Subset of [:S,T:] holds proj1 (downarrow X) = downarrow (proj1 X)
let T be reflexive RelStr ; ::_thesis: for X being Subset of [:S,T:] holds proj1 (downarrow X) = downarrow (proj1 X)
let X be Subset of [:S,T:]; ::_thesis: proj1 (downarrow X) = downarrow (proj1 X)
thus  proj1 (downarrow X) c= downarrow (proj1 X) by Th28; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (proj1 X) c= proj1 (downarrow X)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow (proj1 X) or a in proj1 (downarrow X) )
assume A1: a in downarrow (proj1 X) ; ::_thesis: a in proj1 (downarrow X)
then reconsider S9 = S as non empty RelStr ;
reconsider a9 = a as Element of S9 by A1;
consider b being Element of S9 such that
A2: b >= a9 and
A3: b in proj1 X by A1, WAYBEL_0:def_15;
consider b2 being set  such that
A4: [b,b2] in X by A3, XTUPLE_0:def_12;
A5: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then reconsider T9 = T as non empty reflexive RelStr by A4, ZFMISC_1:87;
reconsider b2 = b2 as Element of T9 by A5, A4, ZFMISC_1:87;
 b2 <= b2 ;
then  [b,b2] >= [a9,b2] by A2, YELLOW_3:11;
then  [a9,b2] in downarrow X by A4, WAYBEL_0:def_15;
hence  a in proj1 (downarrow X) by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: YELLOW10:30
for S being reflexive RelStr
for T being RelStr
for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)
proof
let S be reflexive RelStr ; ::_thesis: for T being RelStr
for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)
let T be RelStr ; ::_thesis: for X being Subset of [:S,T:] holds proj2 (downarrow X) = downarrow (proj2 X)
let X be Subset of [:S,T:]; ::_thesis: proj2 (downarrow X) = downarrow (proj2 X)
thus  proj2 (downarrow X) c= downarrow (proj2 X) by Th28; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (proj2 X) c= proj2 (downarrow X)
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in downarrow (proj2 X) or c in proj2 (downarrow X) )
assume A1: c in downarrow (proj2 X) ; ::_thesis: c in proj2 (downarrow X)
then reconsider T9 = T as non empty RelStr ;
reconsider c9 = c as Element of T9 by A1;
consider b being Element of T9 such that
A2: b >= c9 and
A3: b in proj2 X by A1, WAYBEL_0:def_15;
consider b1 being set  such that
A4: [b1,b] in X by A3, XTUPLE_0:def_13;
A5: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then reconsider S9 = S as non empty reflexive RelStr by A4, ZFMISC_1:87;
reconsider b1 = b1 as Element of S9 by A5, A4, ZFMISC_1:87;
 b1 <= b1 ;
then  [b1,b] >= [b1,c9] by A2, YELLOW_3:11;
then  [b1,c9] in downarrow X by A4, WAYBEL_0:def_15;
hence  c in proj2 (downarrow X) by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: YELLOW10:31
for S, T being RelStr
for X being Subset of [:S,T:] holds uparrow X c= [:(uparrow (proj1 X)),(uparrow (proj2 X)):]
proof
let S, T be RelStr ; ::_thesis: for X being Subset of [:S,T:] holds uparrow X c= [:(uparrow (proj1 X)),(uparrow (proj2 X)):]
let X be Subset of [:S,T:]; ::_thesis: uparrow X c= [:(uparrow (proj1 X)),(uparrow (proj2 X)):]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow X or x in [:(uparrow (proj1 X)),(uparrow (proj2 X)):] )
assume A1: x in uparrow X ; ::_thesis: x in [:(uparrow (proj1 X)),(uparrow (proj2 X)):]
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ex a, b being set st
( a in the carrier of S & b in the carrier of T & x = [a,b] ) by A1, ZFMISC_1:def_2;
then reconsider S9 = S, T9 = T as non empty RelStr ;
reconsider x9 = x as Element of [:S9,T9:] by A1;
consider y being Element of [:S9,T9:] such that
A3: y <= x9 and
A4: y in X by A1, WAYBEL_0:def_16;
A5: y `1 <= x9 `1 by A3, YELLOW_3:12;
A6: y = [(y `1),(y `2)] by A2, MCART_1:21;
then  y `1 in proj1 X by A4, XTUPLE_0:def_12;
then A7: x `1 in uparrow (proj1 X) by A5, WAYBEL_0:def_16;
A8: y `2 <= x9 `2 by A3, YELLOW_3:12;
 y `2 in proj2 X by A4, A6, XTUPLE_0:def_13;
then A9: x `2 in uparrow (proj2 X) by A8, WAYBEL_0:def_16;
 x9 = [(x9 `1),(x9 `2)] by A2, MCART_1:21;
hence  x in [:(uparrow (proj1 X)),(uparrow (proj2 X)):] by A7, A9, MCART_1:11; ::_thesis: verum
end;

theorem :: YELLOW10:32
for S, T being RelStr
for X being Subset of S
for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]
proof
let S, T be RelStr ; ::_thesis: for X being Subset of S
for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]
let X be Subset of S; ::_thesis: for Y being Subset of T holds [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]
let Y be Subset of T; ::_thesis: [:(uparrow X),(uparrow Y):] = uparrow [:X,Y:]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: uparrow [:X,Y:] c= [:(uparrow X),(uparrow Y):]
let x be set ; ::_thesis: ( x in [:(uparrow X),(uparrow Y):] implies x in uparrow [:X,Y:] )
assume  x in [:(uparrow X),(uparrow Y):] ; ::_thesis: x in uparrow [:X,Y:]
then consider x1, x2 being set  such that
A1: x1 in uparrow X and
A2: x2 in uparrow Y and
A3: x = [x1,x2] by ZFMISC_1:def_2;
reconsider S9 = S, T9 = T as non empty RelStr by A1, A2;
reconsider x1 = x1 as Element of S9 by A1;
consider y1 being Element of S9 such that
A4: ( y1 <= x1 & y1 in X ) by A1, WAYBEL_0:def_16;
reconsider x2 = x2 as Element of T9 by A2;
consider y2 being Element of T9 such that
A5: ( y2 <= x2 & y2 in Y ) by A2, WAYBEL_0:def_16;
 ( [y1,y2] in [:X,Y:] & [y1,y2] <= [x1,x2] ) by A4, A5, YELLOW_3:11, ZFMISC_1:87;
hence  x in uparrow [:X,Y:] by A3, WAYBEL_0:def_16; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow [:X,Y:] or x in [:(uparrow X),(uparrow Y):] )
assume A6: x in uparrow [:X,Y:] ; ::_thesis: x in [:(uparrow X),(uparrow Y):]
A7: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  ex a, b being set st
( a in the carrier of S & b in the carrier of T & x = [a,b] ) by A6, ZFMISC_1:def_2;
then reconsider S9 = S, T9 = T as non empty RelStr ;
reconsider x9 = x as Element of [:S9,T9:] by A6;
consider y being Element of [:S9,T9:] such that
A8: ( y <= x9 & y in [:X,Y:] ) by A6, WAYBEL_0:def_16;
 ( y `2 <= x9 `2 & y `2 in Y ) by A8, MCART_1:10, YELLOW_3:12;
then A9: x `2 in uparrow Y by WAYBEL_0:def_16;
 ( y `1 <= x9 `1 & y `1 in X ) by A8, MCART_1:10, YELLOW_3:12;
then A10: x `1 in uparrow X by WAYBEL_0:def_16;
 x9 = [(x9 `1),(x9 `2)] by A7, MCART_1:21;
hence  x in [:(uparrow X),(uparrow Y):] by A10, A9, MCART_1:11; ::_thesis: verum
end;

theorem Th33: :: YELLOW10:33
for S, T being RelStr
for 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 ; ::_thesis: for X being Subset of [:S,T:] holds
( proj1 (uparrow X) c= uparrow (proj1 X) & proj2 (uparrow X) c= uparrow (proj2 X) )
let X be Subset of [:S,T:]; ::_thesis: ( proj1 (uparrow X) c= uparrow (proj1 X) & proj2 (uparrow X) c= uparrow (proj2 X) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
hereby  :: according to TARSKI:def_3 ::_thesis: proj2 (uparrow X) c= uparrow (proj2 X)
let a be set ; ::_thesis: ( a in proj1 (uparrow X) implies a in uparrow (proj1 X) )
assume  a in proj1 (uparrow X) ; ::_thesis: a in uparrow (proj1 X)
then consider b being set  such that
A2: [a,b] in uparrow X by XTUPLE_0:def_12;
reconsider S9 = S, T9 = T as non empty RelStr by A1, A2, ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1, A2, ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1, A2, ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A3: ( [a9,b9] >= c & c in X ) by A2, WAYBEL_0:def_16;
 c = [(c `1),(c `2)] by A1, MCART_1:21;
then  ( a9 >= c `1 & c `1 in proj1 X ) by A3, XTUPLE_0:def_12, YELLOW_3:11;
hence  a in uparrow (proj1 X) by WAYBEL_0:def_16; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in proj2 (uparrow X) or b in uparrow (proj2 X) )
assume  b in proj2 (uparrow X) ; ::_thesis: b in uparrow (proj2 X)
then consider a being set  such that
A4: [a,b] in uparrow X by XTUPLE_0:def_13;
reconsider S9 = S, T9 = T as non empty RelStr by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T9 by A1, A4, ZFMISC_1:87;
reconsider a9 = a as Element of S9 by A1, A4, ZFMISC_1:87;
consider c being Element of [:S9,T9:] such that
A5: ( [a9,b9] >= c & c in X ) by A4, WAYBEL_0:def_16;
 c = [(c `1),(c `2)] by A1, MCART_1:21;
then  ( b9 >= c `2 & c `2 in proj2 X ) by A5, XTUPLE_0:def_13, YELLOW_3:11;
hence  b in uparrow (proj2 X) by WAYBEL_0:def_16; ::_thesis: verum
end;

theorem :: YELLOW10:34
for S being RelStr
for T being reflexive RelStr
for X being Subset of [:S,T:] holds proj1 (uparrow X) = uparrow (proj1 X)
proof
let S be RelStr ; ::_thesis: for T being reflexive RelStr
for X being Subset of [:S,T:] holds proj1 (uparrow X) = uparrow (proj1 X)
let T be reflexive RelStr ; ::_thesis: for X being Subset of [:S,T:] holds proj1 (uparrow X) = uparrow (proj1 X)
let X be Subset of [:S,T:]; ::_thesis: proj1 (uparrow X) = uparrow (proj1 X)
thus  proj1 (uparrow X) c= uparrow (proj1 X) by Th33; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (proj1 X) c= proj1 (uparrow X)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in uparrow (proj1 X) or a in proj1 (uparrow X) )
assume A1: a in uparrow (proj1 X) ; ::_thesis: a in proj1 (uparrow X)
then reconsider S9 = S as non empty RelStr ;
reconsider a9 = a as Element of S9 by A1;
consider b being Element of S9 such that
A2: b <= a9 and
A3: b in proj1 X by A1, WAYBEL_0:def_16;
consider b2 being set  such that
A4: [b,b2] in X by A3, XTUPLE_0:def_12;
A5: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then reconsider T9 = T as non empty reflexive RelStr by A4, ZFMISC_1:87;
reconsider b2 = b2 as Element of T9 by A5, A4, ZFMISC_1:87;
 b2 <= b2 ;
then  [b,b2] <= [a9,b2] by A2, YELLOW_3:11;
then  [a9,b2] in uparrow X by A4, WAYBEL_0:def_16;
hence  a in proj1 (uparrow X) by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: YELLOW10:35
for S being reflexive RelStr
for T being RelStr
for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)
proof
let S be reflexive RelStr ; ::_thesis: for T being RelStr
for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)
let T be RelStr ; ::_thesis: for X being Subset of [:S,T:] holds proj2 (uparrow X) = uparrow (proj2 X)
let X be Subset of [:S,T:]; ::_thesis: proj2 (uparrow X) = uparrow (proj2 X)
thus  proj2 (uparrow X) c= uparrow (proj2 X) by Th33; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (proj2 X) c= proj2 (uparrow X)
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in uparrow (proj2 X) or c in proj2 (uparrow X) )
assume A1: c in uparrow (proj2 X) ; ::_thesis: c in proj2 (uparrow X)
then reconsider T9 = T as non empty RelStr ;
reconsider c9 = c as Element of T9 by A1;
consider b being Element of T9 such that
A2: b <= c9 and
A3: b in proj2 X by A1, WAYBEL_0:def_16;
consider b1 being set  such that
A4: [b1,b] in X by A3, XTUPLE_0:def_13;
A5: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then reconsider S9 = S as non empty reflexive RelStr by A4, ZFMISC_1:87;
reconsider b1 = b1 as Element of S9 by A5, A4, ZFMISC_1:87;
 b1 <= b1 ;
then  [b1,b] <= [b1,c9] by A2, YELLOW_3:11;
then  [b1,c9] in uparrow X by A4, WAYBEL_0:def_16;
hence  c in proj2 (uparrow X) by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: YELLOW10:36
for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]
proof
let S, T be non empty RelStr ; ::_thesis: for s being Element of S
for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]
let s be Element of S; ::_thesis: for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]
let t be Element of T; ::_thesis: [:(downarrow s),(downarrow t):] = downarrow [s,t]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: downarrow [s,t] c= [:(downarrow s),(downarrow t):]
let x be set ; ::_thesis: ( x in [:(downarrow s),(downarrow t):] implies x in downarrow [s,t] )
assume  x in [:(downarrow s),(downarrow t):] ; ::_thesis: x in downarrow [s,t]
then consider x1, x2 being set  such that
A1: x1 in downarrow s and
A2: x2 in downarrow t and
A3: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Element of T by A2;
reconsider x1 = x1 as Element of S by A1;
 ( s >= x1 & t >= x2 ) by A1, A2, WAYBEL_0:17;
then  [s,t] >= [x1,x2] by YELLOW_3:11;
hence  x in downarrow [s,t] by A3, WAYBEL_0:17; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow [s,t] or x in [:(downarrow s),(downarrow t):] )
assume A4: x in downarrow [s,t] ; ::_thesis: x in [:(downarrow s),(downarrow t):]
then reconsider x9 = x as Element of [:S,T:] ;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A5: x9 = [(x9 `1),(x9 `2)] by MCART_1:21;
A6: [s,t] >= x9 by A4, WAYBEL_0:17;
then  t >= x9 `2 by A5, YELLOW_3:11;
then A7: x `2 in downarrow t by WAYBEL_0:17;
 s >= x9 `1 by A5, A6, YELLOW_3:11;
then  x `1 in downarrow s by WAYBEL_0:17;
hence  x in [:(downarrow s),(downarrow t):] by A5, A7, MCART_1:11; ::_thesis: verum
end;

theorem Th37: :: YELLOW10:37
for S, T being non empty RelStr
for 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 ; ::_thesis: for x being Element of [:S,T:] holds
( proj1 (downarrow x) c= downarrow (x `1) & proj2 (downarrow x) c= downarrow (x `2) )
let x be Element of [:S,T:]; ::_thesis: ( proj1 (downarrow x) c= downarrow (x `1) & proj2 (downarrow x) c= downarrow (x `2) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
hereby  :: according to TARSKI:def_3 ::_thesis: proj2 (downarrow x) c= downarrow (x `2)
let a be set ; ::_thesis: ( a in proj1 (downarrow x) implies a in downarrow (x `1) )
assume  a in proj1 (downarrow x) ; ::_thesis: a in downarrow (x `1)
then consider b being set  such that
A3: [a,b] in downarrow x by XTUPLE_0:def_12;
reconsider b = b as Element of T by A1, A3, ZFMISC_1:87;
reconsider a9 = a as Element of S by A1, A3, ZFMISC_1:87;
 [a9,b] <= x by A3, WAYBEL_0:17;
then  a9 <= x `1 by A2, YELLOW_3:11;
hence  a in downarrow (x `1) by WAYBEL_0:17; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in proj2 (downarrow x) or b in downarrow (x `2) )
assume  b in proj2 (downarrow x) ; ::_thesis: b in downarrow (x `2)
then consider a being set  such that
A4: [a,b] in downarrow x by XTUPLE_0:def_13;
reconsider a = a as Element of S by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A4, ZFMISC_1:87;
 [a,b9] <= x by A4, WAYBEL_0:17;
then  b9 <= x `2 by A2, YELLOW_3:11;
hence  b in downarrow (x `2) by WAYBEL_0:17; ::_thesis: verum
end;

theorem :: YELLOW10:38
for S being non empty RelStr
for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)
let T be non empty reflexive RelStr ; ::_thesis: for x being Element of [:S,T:] holds proj1 (downarrow x) = downarrow (x `1)
let x be Element of [:S,T:]; ::_thesis: proj1 (downarrow x) = downarrow (x `1)
A1: x `2 <= x `2 ;
thus  proj1 (downarrow x) c= downarrow (x `1) by Th37; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (x `1) c= proj1 (downarrow x)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow (x `1) or a in proj1 (downarrow x) )
assume A2: a in downarrow (x `1) ; ::_thesis: a in proj1 (downarrow x)
then reconsider a9 = a as Element of S ;
 a9 <= x `1 by A2, WAYBEL_0:17;
then  [a9,(x `2)] <= [(x `1),(x `2)] by A1, YELLOW_3:11;
then A3: [a9,(x `2)] in downarrow [(x `1),(x `2)] by WAYBEL_0:17;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  x = [(x `1),(x `2)] by MCART_1:21;
hence  a in proj1 (downarrow x) by A3, XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: YELLOW10:39
for S being non empty reflexive RelStr
for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (downarrow x) = downarrow (x `2)
proof
let S be non empty reflexive RelStr ; ::_thesis: for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (downarrow x) = downarrow (x `2)
let T be non empty RelStr ; ::_thesis: for x being Element of [:S,T:] holds proj2 (downarrow x) = downarrow (x `2)
let x be Element of [:S,T:]; ::_thesis: proj2 (downarrow x) = downarrow (x `2)
A1: x `1 <= x `1 ;
thus  proj2 (downarrow x) c= downarrow (x `2) by Th37; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (x `2) c= proj2 (downarrow x)
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in downarrow (x `2) or b in proj2 (downarrow x) )
assume A2: b in downarrow (x `2) ; ::_thesis: b in proj2 (downarrow x)
then reconsider b9 = b as Element of T ;
 b9 <= x `2 by A2, WAYBEL_0:17;
then  [(x `1),b9] <= [(x `1),(x `2)] by A1, YELLOW_3:11;
then A3: [(x `1),b9] in downarrow [(x `1),(x `2)] by WAYBEL_0:17;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  x = [(x `1),(x `2)] by MCART_1:21;
hence  b in proj2 (downarrow x) by A3, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: YELLOW10:40
for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds [:(uparrow s),(uparrow t):] = uparrow [s,t]
proof
let S, T be non empty RelStr ; ::_thesis: for s being Element of S
for t being Element of T holds [:(uparrow s),(uparrow t):] = uparrow [s,t]
let s be Element of S; ::_thesis: for t being Element of T holds [:(uparrow s),(uparrow t):] = uparrow [s,t]
let t be Element of T; ::_thesis: [:(uparrow s),(uparrow t):] = uparrow [s,t]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: uparrow [s,t] c= [:(uparrow s),(uparrow t):]
let x be set ; ::_thesis: ( x in [:(uparrow s),(uparrow t):] implies x in uparrow [s,t] )
assume  x in [:(uparrow s),(uparrow t):] ; ::_thesis: x in uparrow [s,t]
then consider x1, x2 being set  such that
A1: x1 in uparrow s and
A2: x2 in uparrow t and
A3: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Element of T by A2;
reconsider x1 = x1 as Element of S by A1;
 ( s <= x1 & t <= x2 ) by A1, A2, WAYBEL_0:18;
then  [s,t] <= [x1,x2] by YELLOW_3:11;
hence  x in uparrow [s,t] by A3, WAYBEL_0:18; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow [s,t] or x in [:(uparrow s),(uparrow t):] )
assume A4: x in uparrow [s,t] ; ::_thesis: x in [:(uparrow s),(uparrow t):]
then reconsider x9 = x as Element of [:S,T:] ;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A5: x9 = [(x9 `1),(x9 `2)] by MCART_1:21;
A6: [s,t] <= x9 by A4, WAYBEL_0:18;
then  t <= x9 `2 by A5, YELLOW_3:11;
then A7: x `2 in uparrow t by WAYBEL_0:18;
 s <= x9 `1 by A5, A6, YELLOW_3:11;
then  x `1 in uparrow s by WAYBEL_0:18;
hence  x in [:(uparrow s),(uparrow t):] by A5, A7, MCART_1:11; ::_thesis: verum
end;

theorem Th41: :: YELLOW10:41
for S, T being non empty RelStr
for 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 ; ::_thesis: for x being Element of [:S,T:] holds
( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )
let x be Element of [:S,T:]; ::_thesis: ( proj1 (uparrow x) c= uparrow (x `1) & proj2 (uparrow x) c= uparrow (x `2) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
hereby  :: according to TARSKI:def_3 ::_thesis: proj2 (uparrow x) c= uparrow (x `2)
let a be set ; ::_thesis: ( a in proj1 (uparrow x) implies a in uparrow (x `1) )
assume  a in proj1 (uparrow x) ; ::_thesis: a in uparrow (x `1)
then consider b being set  such that
A3: [a,b] in uparrow x by XTUPLE_0:def_12;
reconsider b = b as Element of T by A1, A3, ZFMISC_1:87;
reconsider a9 = a as Element of S by A1, A3, ZFMISC_1:87;
 [a9,b] >= x by A3, WAYBEL_0:18;
then  a9 >= x `1 by A2, YELLOW_3:11;
hence  a in uparrow (x `1) by WAYBEL_0:18; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in proj2 (uparrow x) or b in uparrow (x `2) )
assume  b in proj2 (uparrow x) ; ::_thesis: b in uparrow (x `2)
then consider a being set  such that
A4: [a,b] in uparrow x by XTUPLE_0:def_13;
reconsider a = a as Element of S by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A4, ZFMISC_1:87;
 [a,b9] >= x by A4, WAYBEL_0:18;
then  b9 >= x `2 by A2, YELLOW_3:11;
hence  b in uparrow (x `2) by WAYBEL_0:18; ::_thesis: verum
end;

theorem :: YELLOW10:42
for S being non empty RelStr
for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive RelStr
for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1)
let T be non empty reflexive RelStr ; ::_thesis: for x being Element of [:S,T:] holds proj1 (uparrow x) = uparrow (x `1)
let x be Element of [:S,T:]; ::_thesis: proj1 (uparrow x) = uparrow (x `1)
A1: x `2 <= x `2 ;
thus  proj1 (uparrow x) c= uparrow (x `1) by Th41; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (x `1) c= proj1 (uparrow x)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in uparrow (x `1) or a in proj1 (uparrow x) )
assume A2: a in uparrow (x `1) ; ::_thesis: a in proj1 (uparrow x)
then reconsider a9 = a as Element of S ;
 a9 >= x `1 by A2, WAYBEL_0:18;
then  [a9,(x `2)] >= [(x `1),(x `2)] by A1, YELLOW_3:11;
then A3: [a9,(x `2)] in uparrow [(x `1),(x `2)] by WAYBEL_0:18;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  x = [(x `1),(x `2)] by MCART_1:21;
hence  a in proj1 (uparrow x) by A3, XTUPLE_0:def_12; ::_thesis: verum
end;

theorem :: YELLOW10:43
for S being non empty reflexive RelStr
for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)
proof
let S be non empty reflexive RelStr ; ::_thesis: for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)
let T be non empty RelStr ; ::_thesis: for x being Element of [:S,T:] holds proj2 (uparrow x) = uparrow (x `2)
let x be Element of [:S,T:]; ::_thesis: proj2 (uparrow x) = uparrow (x `2)
A1: x `1 <= x `1 ;
thus  proj2 (uparrow x) c= uparrow (x `2) by Th41; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (x `2) c= proj2 (uparrow x)
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in uparrow (x `2) or b in proj2 (uparrow x) )
assume A2: b in uparrow (x `2) ; ::_thesis: b in proj2 (uparrow x)
then reconsider b9 = b as Element of T ;
 b9 >= x `2 by A2, WAYBEL_0:18;
then  [(x `1),b9] >= [(x `1),(x `2)] by A1, YELLOW_3:11;
then A3: [(x `1),b9] in uparrow [(x `1),(x `2)] by WAYBEL_0:18;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  x = [(x `1),(x `2)] by MCART_1:21;
hence  b in proj2 (uparrow x) by A3, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th44: :: YELLOW10:44
for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(waybelow s),(waybelow t):] = waybelow [s,t]
proof
let S, T be non empty up-complete Poset; ::_thesis: for s being Element of S
for t being Element of T holds [:(waybelow s),(waybelow t):] = waybelow [s,t]
let s be Element of S; ::_thesis: for t being Element of T holds [:(waybelow s),(waybelow t):] = waybelow [s,t]
let t be Element of T; ::_thesis: [:(waybelow s),(waybelow t):] = waybelow [s,t]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: waybelow [s,t] c= [:(waybelow s),(waybelow t):]
let x be set ; ::_thesis: ( x in [:(waybelow s),(waybelow t):] implies x in waybelow [s,t] )
assume  x in [:(waybelow s),(waybelow t):] ; ::_thesis: x in waybelow [s,t]
then consider x1, x2 being set  such that
A1: x1 in waybelow s and
A2: x2 in waybelow t and
A3: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Element of T by A2;
reconsider x1 = x1 as Element of S by A1;
 ( s >> x1 & t >> x2 ) by A1, A2, WAYBEL_3:7;
then  [s,t] >> [x1,x2] by Th19;
hence  x in waybelow [s,t] by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in waybelow [s,t] or x in [:(waybelow s),(waybelow t):] )
assume A4: x in waybelow [s,t] ; ::_thesis: x in [:(waybelow s),(waybelow t):]
then reconsider x9 = x as Element of [:S,T:] ;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A5: x9 = [(x9 `1),(x9 `2)] by MCART_1:21;
A6: [s,t] >> x9 by A4, WAYBEL_3:7;
then  t >> x9 `2 by A5, Th19;
then A7: x `2 in waybelow t ;
 s >> x9 `1 by A5, A6, Th19;
then  x `1 in waybelow s ;
hence  x in [:(waybelow s),(waybelow t):] by A5, A7, MCART_1:11; ::_thesis: verum
end;

theorem Th45: :: YELLOW10:45
for S, T being non empty reflexive antisymmetric up-complete RelStr
for 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 non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for x being Element of [:S,T:] holds
( proj1 (waybelow x) c= waybelow (x `1) & proj2 (waybelow x) c= waybelow (x `2) )
let x be Element of [:S,T:]; ::_thesis: ( proj1 (waybelow x) c= waybelow (x `1) & proj2 (waybelow x) c= waybelow (x `2) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
hereby  :: according to TARSKI:def_3 ::_thesis: proj2 (waybelow x) c= waybelow (x `2)
let a be set ; ::_thesis: ( a in proj1 (waybelow x) implies a in waybelow (x `1) )
assume  a in proj1 (waybelow x) ; ::_thesis: a in waybelow (x `1)
then consider b being set  such that
A3: [a,b] in waybelow x by XTUPLE_0:def_12;
reconsider b = b as Element of T by A1, A3, ZFMISC_1:87;
reconsider a9 = a as Element of S by A1, A3, ZFMISC_1:87;
 [a9,b] << x by A3, WAYBEL_3:7;
then  a9 << x `1 by A2, Th18;
hence  a in waybelow (x `1) ; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in proj2 (waybelow x) or b in waybelow (x `2) )
assume  b in proj2 (waybelow x) ; ::_thesis: b in waybelow (x `2)
then consider a being set  such that
A4: [a,b] in waybelow x by XTUPLE_0:def_13;
reconsider a = a as Element of S by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A4, ZFMISC_1:87;
 [a,b9] << x by A4, WAYBEL_3:7;
then  b9 << x `2 by A2, Th18;
hence  b in waybelow (x `2) ; ::_thesis: verum
end;

theorem Th46: :: YELLOW10:46
for S being non empty up-complete Poset
for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)
proof
let S be non empty up-complete Poset; ::_thesis: for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)
let T be non empty lower-bounded up-complete Poset; ::_thesis: for x being Element of [:S,T:] holds proj1 (waybelow x) = waybelow (x `1)
let x be Element of [:S,T:]; ::_thesis: proj1 (waybelow x) = waybelow (x `1)
A1: Bottom T << x `2 by WAYBEL_3:4;
thus  proj1 (waybelow x) c= waybelow (x `1) by Th45; :: according to XBOOLE_0:def_10 ::_thesis: waybelow (x `1) c= proj1 (waybelow x)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in waybelow (x `1) or a in proj1 (waybelow x) )
assume A2: a in waybelow (x `1) ; ::_thesis: a in proj1 (waybelow x)
then reconsider a9 = a as Element of S ;
 a9 << x `1 by A2, WAYBEL_3:7;
then  [a9,(Bottom T)] << [(x `1),(x `2)] by A1, Th19;
then A3: [a9,(Bottom T)] in waybelow [(x `1),(x `2)] ;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  x = [(x `1),(x `2)] by MCART_1:21;
hence  a in proj1 (waybelow x) by A3, XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th47: :: YELLOW10:47
for S being non empty lower-bounded up-complete Poset
for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2)
proof
let S be non empty lower-bounded up-complete Poset; ::_thesis: for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2)
let T be non empty up-complete Poset; ::_thesis: for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2)
let x be Element of [:S,T:]; ::_thesis: proj2 (waybelow x) = waybelow (x `2)
A1: Bottom S << x `1 by WAYBEL_3:4;
thus  proj2 (waybelow x) c= waybelow (x `2) by Th45; :: according to XBOOLE_0:def_10 ::_thesis: waybelow (x `2) c= proj2 (waybelow x)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in waybelow (x `2) or a in proj2 (waybelow x) )
assume A2: a in waybelow (x `2) ; ::_thesis: a in proj2 (waybelow x)
then reconsider a9 = a as Element of T ;
 a9 << x `2 by A2, WAYBEL_3:7;
then  [(Bottom S),a9] << [(x `1),(x `2)] by A1, Th19;
then A3: [(Bottom S),a9] in waybelow [(x `1),(x `2)] ;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then  x = [(x `1),(x `2)] by MCART_1:21;
hence  a in proj2 (waybelow x) by A3, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: YELLOW10:48
for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]
proof
let S, T be non empty up-complete Poset; ::_thesis: for s being Element of S
for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]
let s be Element of S; ::_thesis: for t being Element of T holds [:(wayabove s),(wayabove t):] = wayabove [s,t]
let t be Element of T; ::_thesis: [:(wayabove s),(wayabove t):] = wayabove [s,t]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: wayabove [s,t] c= [:(wayabove s),(wayabove t):]
let x be set ; ::_thesis: ( x in [:(wayabove s),(wayabove t):] implies x in wayabove [s,t] )
assume  x in [:(wayabove s),(wayabove t):] ; ::_thesis: x in wayabove [s,t]
then consider x1, x2 being set  such that
A1: x1 in wayabove s and
A2: x2 in wayabove t and
A3: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Element of T by A2;
reconsider x1 = x1 as Element of S by A1;
 ( s << x1 & t << x2 ) by A1, A2, WAYBEL_3:8;
then  [s,t] << [x1,x2] by Th19;
hence  x in wayabove [s,t] by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in wayabove [s,t] or x in [:(wayabove s),(wayabove t):] )
assume A4: x in wayabove [s,t] ; ::_thesis: x in [:(wayabove s),(wayabove t):]
then reconsider x9 = x as Element of [:S,T:] ;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A5: x9 = [(x9 `1),(x9 `2)] by MCART_1:21;
A6: [s,t] << x9 by A4, WAYBEL_3:8;
then  t << x9 `2 by A5, Th19;
then A7: x `2 in wayabove t ;
 s << x9 `1 by A5, A6, Th19;
then  x `1 in wayabove s ;
hence  x in [:(wayabove s),(wayabove t):] by A5, A7, MCART_1:11; ::_thesis: verum
end;

theorem :: YELLOW10:49
for S, T being non empty reflexive antisymmetric up-complete RelStr
for 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 non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for x being Element of [:S,T:] holds
( proj1 (wayabove x) c= wayabove (x `1) & proj2 (wayabove x) c= wayabove (x `2) )
let x be Element of [:S,T:]; ::_thesis: ( proj1 (wayabove x) c= wayabove (x `1) & proj2 (wayabove x) c= wayabove (x `2) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
hereby  :: according to TARSKI:def_3 ::_thesis: proj2 (wayabove x) c= wayabove (x `2)
let a be set ; ::_thesis: ( a in proj1 (wayabove x) implies a in wayabove (x `1) )
assume  a in proj1 (wayabove x) ; ::_thesis: a in wayabove (x `1)
then consider b being set  such that
A3: [a,b] in wayabove x by XTUPLE_0:def_12;
reconsider b = b as Element of T by A1, A3, ZFMISC_1:87;
reconsider a9 = a as Element of S by A1, A3, ZFMISC_1:87;
 [a9,b] >> x by A3, WAYBEL_3:8;
then  a9 >> x `1 by A2, Th18;
hence  a in wayabove (x `1) ; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in proj2 (wayabove x) or b in wayabove (x `2) )
assume  b in proj2 (wayabove x) ; ::_thesis: b in wayabove (x `2)
then consider a being set  such that
A4: [a,b] in wayabove x by XTUPLE_0:def_13;
reconsider a = a as Element of S by A1, A4, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A4, ZFMISC_1:87;
 [a,b9] >> x by A4, WAYBEL_3:8;
then  b9 >> x `2 by A2, Th18;
hence  b in wayabove (x `2) ; ::_thesis: verum
end;

theorem Th50: :: YELLOW10:50
for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]
proof
let S, T be non empty up-complete Poset; ::_thesis: for s being Element of S
for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]
let s be Element of S; ::_thesis: for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]
let t be Element of T; ::_thesis: [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: compactbelow [s,t] c= [:(compactbelow s),(compactbelow t):]
let x be set ; ::_thesis: ( x in [:(compactbelow s),(compactbelow t):] implies x in compactbelow [s,t] )
assume  x in [:(compactbelow s),(compactbelow t):] ; ::_thesis: x in compactbelow [s,t]
then consider x1, x2 being set  such that
A1: x1 in compactbelow s and
A2: x2 in compactbelow t and
A3: x = [x1,x2] by ZFMISC_1:def_2;
reconsider x2 = x2 as Element of T by A2;
reconsider x1 = x1 as Element of S by A1;
 ( s >= x1 & t >= x2 ) by A1, A2, WAYBEL_8:4;
then A4: [s,t] >= [x1,x2] by YELLOW_3:11;
A5: ( [x1,x2] `1 = x1 & [x1,x2] `2 = x2 ) ;
 ( x1 is compact & x2 is compact ) by A1, A2, WAYBEL_8:4;
then  [x1,x2] is compact by A5, Th23;
hence  x in compactbelow [s,t] by A3, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in compactbelow [s,t] or x in [:(compactbelow s),(compactbelow t):] )
assume A6: x in compactbelow [s,t] ; ::_thesis: x in [:(compactbelow s),(compactbelow t):]
then reconsider x9 = x as Element of [:S,T:] ;
A7: x9 is compact by A6, WAYBEL_8:4;
then A8: x9 `1 is compact by Th22;
A9: x9 `2 is compact by A7, Th22;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A10: x9 = [(x9 `1),(x9 `2)] by MCART_1:21;
A11: [s,t] >= x9 by A6, WAYBEL_8:4;
then  t >= x9 `2 by A10, YELLOW_3:11;
then A12: x `2 in compactbelow t by A9;
 s >= x9 `1 by A10, A11, YELLOW_3:11;
then  x `1 in compactbelow s by A8;
hence  x in [:(compactbelow s),(compactbelow t):] by A10, A12, MCART_1:11; ::_thesis: verum
end;

theorem Th51: :: YELLOW10:51
for S, T being non empty reflexive antisymmetric up-complete RelStr
for 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 non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for x being Element of [:S,T:] holds
( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )
let x be Element of [:S,T:]; ::_thesis: ( proj1 (compactbelow x) c= compactbelow (x `1) & proj2 (compactbelow x) c= compactbelow (x `2) )
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A2: x = [(x `1),(x `2)] by MCART_1:21;
hereby  :: according to TARSKI:def_3 ::_thesis: proj2 (compactbelow x) c= compactbelow (x `2)
let a be set ; ::_thesis: ( a in proj1 (compactbelow x) implies a in compactbelow (x `1) )
assume  a in proj1 (compactbelow x) ; ::_thesis: a in compactbelow (x `1)
then consider b being set  such that
A3: [a,b] in compactbelow x by XTUPLE_0:def_12;
reconsider b = b as Element of T by A1, A3, ZFMISC_1:87;
reconsider a9 = a as Element of S by A1, A3, ZFMISC_1:87;
 ( [a9,b] `1 = a9 & [a9,b] is compact ) by A3, WAYBEL_8:4;
then A4: a9 is compact by Th22;
 [a9,b] <= x by A3, WAYBEL_8:4;
then  a9 <= x `1 by A2, YELLOW_3:11;
hence  a in compactbelow (x `1) by A4; ::_thesis: verum
end;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in proj2 (compactbelow x) or b in compactbelow (x `2) )
assume  b in proj2 (compactbelow x) ; ::_thesis: b in compactbelow (x `2)
then consider a being set  such that
A5: [a,b] in compactbelow x by XTUPLE_0:def_13;
reconsider a = a as Element of S by A1, A5, ZFMISC_1:87;
reconsider b9 = b as Element of T by A1, A5, ZFMISC_1:87;
 ( [a,b9] `2 = b9 & [a,b9] is compact ) by A5, WAYBEL_8:4;
then A6: b9 is compact by Th22;
 [a,b9] <= x by A5, WAYBEL_8:4;
then  b9 <= x `2 by A2, YELLOW_3:11;
hence  b in compactbelow (x `2) by A6; ::_thesis: verum
end;

theorem Th52: :: YELLOW10:52
for S being non empty up-complete Poset
for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1)
proof
let S be non empty up-complete Poset; ::_thesis: for T being non empty lower-bounded up-complete Poset
for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1)
let T be non empty lower-bounded up-complete Poset; ::_thesis: for x being Element of [:S,T:] holds proj1 (compactbelow x) = compactbelow (x `1)
let x be Element of [:S,T:]; ::_thesis: proj1 (compactbelow x) = compactbelow (x `1)
A1: Bottom T <= x `2 by YELLOW_0:44;
thus  proj1 (compactbelow x) c= compactbelow (x `1) by Th51; :: according to XBOOLE_0:def_10 ::_thesis: compactbelow (x `1) c= proj1 (compactbelow x)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in compactbelow (x `1) or a in proj1 (compactbelow x) )
assume A2: a in compactbelow (x `1) ; ::_thesis: a in proj1 (compactbelow x)
then reconsider a9 = a as Element of S ;
 a9 <= x `1 by A2, WAYBEL_8:4;
then A3: [a9,(Bottom T)] <= [(x `1),(x `2)] by A1, YELLOW_3:11;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A4: x = [(x `1),(x `2)] by MCART_1:21;
A5: ( [a9,(Bottom T)] `1 = a9 & [a9,(Bottom T)] `2 = Bottom T ) ;
 a9 is compact by A2, WAYBEL_8:4;
then  [a9,(Bottom T)] is compact by A5, Th23, WAYBEL_3:15;
then  [a9,(Bottom T)] in compactbelow [(x `1),(x `2)] by A3;
hence  a in proj1 (compactbelow x) by A4, XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th53: :: YELLOW10:53
for S being non empty lower-bounded up-complete Poset
for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (compactbelow x) = compactbelow (x `2)
proof
let S be non empty lower-bounded up-complete Poset; ::_thesis: for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (compactbelow x) = compactbelow (x `2)
let T be non empty up-complete Poset; ::_thesis: for x being Element of [:S,T:] holds proj2 (compactbelow x) = compactbelow (x `2)
let x be Element of [:S,T:]; ::_thesis: proj2 (compactbelow x) = compactbelow (x `2)
A1: Bottom S <= x `1 by YELLOW_0:44;
thus  proj2 (compactbelow x) c= compactbelow (x `2) by Th51; :: according to XBOOLE_0:def_10 ::_thesis: compactbelow (x `2) c= proj2 (compactbelow x)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in compactbelow (x `2) or a in proj2 (compactbelow x) )
assume A2: a in compactbelow (x `2) ; ::_thesis: a in proj2 (compactbelow x)
then reconsider a9 = a as Element of T ;
 a9 <= x `2 by A2, WAYBEL_8:4;
then A3: [(Bottom S),a9] <= [(x `1),(x `2)] by A1, YELLOW_3:11;
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A4: x = [(x `1),(x `2)] by MCART_1:21;
A5: ( [(Bottom S),a9] `1 = Bottom S & [(Bottom S),a9] `2 = a9 ) ;
 a9 is compact by A2, WAYBEL_8:4;
then  [(Bottom S),a9] is compact by A5, Th23, WAYBEL_3:15;
then  [(Bottom S),a9] in compactbelow [(x `1),(x `2)] by A3;
hence  a in proj2 (compactbelow x) by A4, XTUPLE_0:def_13; ::_thesis: verum
end;

registration
let S be non empty reflexive RelStr ;
cluster empty  ->  Open for M2( bool the carrier of S);
coherence
 for b1 being Subset of S st b1 is empty holds
b1 is Open
proof
let X be Subset of S; ::_thesis: ( X is empty implies X is Open )
assume A1: X is empty ; ::_thesis: X is Open
let x be Element of S; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in X or ex b1 being M2( the carrier of S) st
( b1 in X & b1 is_way_below x ) )
assume  x in X ; ::_thesis: ex b1 being M2( the carrier of S) st
( b1 in X & b1 is_way_below x )
hence  ex b1 being M2( the carrier of S) st
( b1 in X & b1 is_way_below x ) by A1; ::_thesis: verum
end;
end;

theorem :: YELLOW10:54
for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is Open holds
( proj1 X is Open & proj2 X is Open )
proof
let S, T be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for X being Subset of [:S,T:] st X is Open holds
( proj1 X is Open & proj2 X is Open )
let X be Subset of [:S,T:]; ::_thesis: ( X is Open implies ( proj1 X is Open & proj2 X is Open ) )
assume A1: for x being Element of [:S,T:] st x in X holds
ex y being Element of [:S,T:] st
( y in X & y << x ) ; :: according to WAYBEL_6:def_1 ::_thesis: ( proj1 X is Open & proj2 X is Open )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
hereby  :: according to WAYBEL_6:def_1 ::_thesis: proj2 X is Open
let s be Element of S; ::_thesis: ( s in proj1 X implies ex z being M2( the carrier of S) st
( z in proj1 X & z << s ) )
assume  s in proj1 X ; ::_thesis: ex z being M2( the carrier of S) st
( z in proj1 X & z << s )
then consider t being set  such that
A3: [s,t] in X by XTUPLE_0:def_12;
reconsider t = t as Element of T by A2, A3, ZFMISC_1:87;
consider y being Element of [:S,T:] such that
A4: y in X and
A5: y << [s,t] by A1, A3;
take z = y `1 ; ::_thesis: ( z in proj1 X & z << s )
A6: y = [(y `1),(y `2)] by A2, MCART_1:21;
hence  z in proj1 X by A4, XTUPLE_0:def_12; ::_thesis: z << s
thus  z << s by A5, A6, Th18; ::_thesis: verum
end;
let t be Element of T; :: according to WAYBEL_6:def_1 ::_thesis: ( not t in proj2 X or ex b1 being M2( the carrier of T) st
( b1 in proj2 X & b1 is_way_below t ) )
assume  t in proj2 X ; ::_thesis: ex b1 being M2( the carrier of T) st
( b1 in proj2 X & b1 is_way_below t )
then consider s being set  such that
A7: [s,t] in X by XTUPLE_0:def_13;
reconsider s = s as Element of S by A2, A7, ZFMISC_1:87;
consider y being Element of [:S,T:] such that
A8: y in X and
A9: y << [s,t] by A1, A7;
take z = y `2 ; ::_thesis: ( z in proj2 X & z is_way_below t )
A10: y = [(y `1),(y `2)] by A2, MCART_1:21;
hence  z in proj2 X by A8, XTUPLE_0:def_13; ::_thesis: z is_way_below t
thus  z is_way_below t by A9, A10, Th18; ::_thesis: verum
end;

theorem :: YELLOW10:55
for S, T being non empty up-complete Poset
for X being Subset of S
for Y being Subset of T st X is Open & Y is Open holds
[:X,Y:] is Open
proof
let S, T be non empty up-complete Poset; ::_thesis: for X being Subset of S
for Y being Subset of T st X is Open & Y is Open holds
[:X,Y:] is Open
let X be Subset of S; ::_thesis: for Y being Subset of T st X is Open & Y is Open holds
[:X,Y:] is Open
let Y be Subset of T; ::_thesis: ( X is Open & Y is Open implies [:X,Y:] is Open )
assume that
A1: for x being Element of S st x in X holds
ex y being Element of S st
( y in X & y << x ) and
A2: for x being Element of T st x in Y holds
ex y being Element of T st
( y in Y & y << x ) ; :: according to WAYBEL_6:def_1 ::_thesis: [:X,Y:] is Open
let x be Element of [:S,T:]; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in [:X,Y:] or ex b1 being M2( the carrier of [:S,T:]) st
( b1 in [:X,Y:] & b1 is_way_below x ) )
assume A3: x in [:X,Y:] ; ::_thesis: ex b1 being M2( the carrier of [:S,T:]) st
( b1 in [:X,Y:] & b1 is_way_below x )
then A4: x = [(x `1),(x `2)] by MCART_1:21;
then  x `1 in X by A3, ZFMISC_1:87;
then consider s being Element of S such that
A5: s in X and
A6: s << x `1 by A1;
 x `2 in Y by A3, A4, ZFMISC_1:87;
then consider t being Element of T such that
A7: t in Y and
A8: t << x `2 by A2;
reconsider t = t as Element of T ;
take  [s,t] ; ::_thesis: ( [s,t] in [:X,Y:] & [s,t] is_way_below x )
thus  [s,t] in [:X,Y:] by A5, A7, ZFMISC_1:87; ::_thesis: [s,t] is_way_below x
thus  [s,t] is_way_below x by A4, A6, A8, Th19; ::_thesis: verum
end;

theorem :: YELLOW10:56
for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is inaccessible holds
( proj1 X is inaccessible & proj2 X is inaccessible )
proof
let S, T be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for X being Subset of [:S,T:] st X is inaccessible holds
( proj1 X is inaccessible & proj2 X is inaccessible )
let X be Subset of [:S,T:]; ::_thesis: ( X is inaccessible implies ( proj1 X is inaccessible & proj2 X is inaccessible ) )
assume A1: for D being non empty directed Subset of [:S,T:] st sup D in X holds
D meets X ; :: according to WAYBEL11:def_1 ::_thesis: ( proj1 X is inaccessible & proj2 X is inaccessible )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
hereby  :: according to WAYBEL11:def_1 ::_thesis: proj2 X is inaccessible
let D be non empty directed Subset of S; ::_thesis: ( sup D in proj1 X implies D meets proj1 X )
assume  sup D in proj1 X ; ::_thesis: D meets proj1 X
then consider t being set  such that
A3: [(sup D),t] in X by XTUPLE_0:def_12;
A4: t in the carrier of T by A2, A3, ZFMISC_1:87;
then reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0:5;
 ex_sup_of [:D,t9:],[:S,T:] by WAYBEL_0:75;
then  sup [:D,t9:] = [(sup (proj1 [:D,t9:])),(sup (proj2 [:D,t9:]))] by YELLOW_3:46
.= [(sup D),(sup (proj2 [:D,t9:]))] by FUNCT_5:9
.= [(sup D),(sup t9)] by FUNCT_5:9
.= [(sup D),t] by A4, YELLOW_0:39 ;
then  [:D,{t}:] meets X by A1, A3;
then consider x being set  such that
A5: x in [:D,{t}:] and
A6: x in X by XBOOLE_0:3;
now__::_thesis:_ex_a_being_set_st_
(_a_in_D_&_a_in_proj1_X_)
take a = x `1 ; ::_thesis: ( a in D & a in proj1 X )
 x = [a,(x `2)] by A5, MCART_1:21;
hence  ( a in D & a in proj1 X ) by A5, A6, XTUPLE_0:def_12, ZFMISC_1:87; ::_thesis: verum
end;
hence  D meets proj1 X by XBOOLE_0:3; ::_thesis: verum
end;
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,T) in proj2 X or not D misses proj2 X )
assume  sup D in proj2 X ; ::_thesis: not D misses proj2 X
then consider s being set  such that
A7: [s,(sup D)] in X by XTUPLE_0:def_13;
A8: s in the carrier of S by A2, A7, ZFMISC_1:87;
then reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0:5;
 ex_sup_of [:s9,D:],[:S,T:] by WAYBEL_0:75;
then  sup [:s9,D:] = [(sup (proj1 [:s9,D:])),(sup (proj2 [:s9,D:]))] by YELLOW_3:46
.= [(sup s9),(sup (proj2 [:s9,D:]))] by FUNCT_5:9
.= [(sup s9),(sup D)] by FUNCT_5:9
.= [s,(sup D)] by A8, YELLOW_0:39 ;
then  [:{s},D:] meets X by A1, A7;
then consider x being set  such that
A9: x in [:{s},D:] and
A10: x in X by XBOOLE_0:3;
now__::_thesis:_ex_a_being_set_st_
(_a_in_D_&_a_in_proj2_X_)
take a = x `2 ; ::_thesis: ( a in D & a in proj2 X )
 x = [(x `1),a] by A9, MCART_1:21;
hence  ( a in D & a in proj2 X ) by A9, A10, XTUPLE_0:def_13, ZFMISC_1:87; ::_thesis: verum
end;
hence  not D misses proj2 X by XBOOLE_0:3; ::_thesis: verum
end;

theorem :: YELLOW10:57
for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being upper Subset of S
for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible
proof
let S, T be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for X being upper Subset of S
for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible
let X be upper Subset of S; ::_thesis: for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible
let Y be upper Subset of T; ::_thesis: ( X is inaccessible & Y is inaccessible implies [:X,Y:] is inaccessible )
assume 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 ; :: according to WAYBEL11:def_1 ::_thesis: [:X,Y:] is inaccessible
let D be non empty directed Subset of [:S,T:]; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,[:S,T:]) in [:X,Y:] or not D misses [:X,Y:] )
assume A3: sup D in [:X,Y:] ; ::_thesis: not D misses [:X,Y:]
 ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A4: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
then  ( not proj1 D is empty & proj1 D is directed & sup (proj1 D) in X ) by A3, YELLOW_3:21, YELLOW_3:22, ZFMISC_1:87;
then  proj1 D meets X by A1;
then consider s being set  such that
A5: s in proj1 D and
A6: s in X by XBOOLE_0:3;
reconsider s = s as Element of S by A5;
consider s2 being set  such that
A7: [s,s2] in D by A5, XTUPLE_0:def_12;
 ( not proj2 D is empty & proj2 D is directed & sup (proj2 D) in Y ) by A3, A4, YELLOW_3:21, YELLOW_3:22, ZFMISC_1:87;
then  proj2 D meets Y by A2;
then consider t being set  such that
A8: t in proj2 D and
A9: t in Y by XBOOLE_0:3;
reconsider t = t as Element of T by A8;
consider t1 being set  such that
A10: [t1,t] in D by A8, XTUPLE_0:def_13;
A11: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then reconsider s2 = s2 as Element of T by A7, ZFMISC_1:87;
reconsider t1 = t1 as Element of S by A11, A10, ZFMISC_1:87;
consider z being Element of [:S,T:] such that
A12: z in D and
A13: [s,s2] <= z and
A14: [t1,t] <= z by A7, A10, WAYBEL_0:def_1;
now__::_thesis:_ex_z_being_Element_of_[:S,T:]_st_
(_z_in_D_&_z_in_[:X,Y:]_)
take z = z; ::_thesis: ( z in D & z in [:X,Y:] )
thus  z in D by A12; ::_thesis: z in [:X,Y:]
A15: z = [(z `1),(z `2)] by A11, MCART_1:21;
then  t <= z `2 by A14, YELLOW_3:11;
then A16: z `2 in Y by A9, WAYBEL_0:def_20;
 s <= z `1 by A13, A15, YELLOW_3:11;
then  z `1 in X by A6, WAYBEL_0:def_20;
hence  z in [:X,Y:] by A15, A16, ZFMISC_1:87; ::_thesis: verum
end;
hence  not D misses [:X,Y:] by XBOOLE_0:3; ::_thesis: verum
end;

theorem :: YELLOW10:58
for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of S
for 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 non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for X being Subset of S
for Y being Subset of T st [:X,Y:] is directly_closed holds
( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )
let X be Subset of S; ::_thesis: for Y being Subset of T st [:X,Y:] is directly_closed holds
( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )
let Y be Subset of T; ::_thesis: ( [:X,Y:] is directly_closed implies ( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) ) )
assume A1: for D being non empty directed Subset of [:S,T:] st D c= [:X,Y:] holds
sup D in [:X,Y:] ; :: according to WAYBEL11:def_2 ::_thesis: ( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )
hereby  ::_thesis: ( X <> {} implies Y is directly_closed )
assume A2: Y <> {} ; ::_thesis: X is directly_closed
thus  X is directly_closed ::_thesis: verum
proof
consider t being set  such that
A3: t in Y by A2, XBOOLE_0:def_1;
reconsider t9 = {t} as non empty directed Subset of T by A3, WAYBEL_0:5;
A4: t9 c= Y by A3, ZFMISC_1:31;
let D be non empty directed Subset of S; :: according to WAYBEL11:def_2 ::_thesis: ( not D c= X or "\/" (D,S) in X )
assume  D c= X ; ::_thesis: "\/" (D,S) in X
then A5: sup [:D,t9:] in [:X,Y:] by A1, A4, ZFMISC_1:96;
 ex_sup_of [:D,t9:],[:S,T:] by WAYBEL_0:75;
then  sup [:D,t9:] = [(sup (proj1 [:D,t9:])),(sup (proj2 [:D,t9:]))] by YELLOW_3:46
.= [(sup D),(sup (proj2 [:D,t9:]))] by FUNCT_5:9
.= [(sup D),(sup t9)] by FUNCT_5:9
.= [(sup D),t] by A3, YELLOW_0:39 ;
hence  "\/" (D,S) in X by A5, ZFMISC_1:87; ::_thesis: verum
end;
end;
assume  X <> {} ; ::_thesis: Y is directly_closed
then consider s being set  such that
A6: s in X by XBOOLE_0:def_1;
reconsider s9 = {s} as non empty directed Subset of S by A6, WAYBEL_0:5;
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( not D c= Y or "\/" (D,T) in Y )
assume A7: D c= Y ; ::_thesis: "\/" (D,T) in Y
 ex_sup_of [:s9,D:],[:S,T:] by WAYBEL_0:75;
then A8: sup [:s9,D:] = [(sup (proj1 [:s9,D:])),(sup (proj2 [:s9,D:]))] by YELLOW_3:46
.= [(sup s9),(sup (proj2 [:s9,D:]))] by FUNCT_5:9
.= [(sup s9),(sup D)] by FUNCT_5:9
.= [s,(sup D)] by A6, YELLOW_0:39 ;
 s9 c= X by A6, ZFMISC_1:31;
then  sup [:s9,D:] in [:X,Y:] by A1, A7, ZFMISC_1:96;
hence  "\/" (D,T) in Y by A8, ZFMISC_1:87; ::_thesis: verum
end;

theorem :: YELLOW10:59
for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of S
for 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 non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for X being Subset of S
for Y being Subset of T st X is directly_closed & Y is directly_closed holds
[:X,Y:] is directly_closed
let X be Subset of S; ::_thesis: for Y being Subset of T st X is directly_closed & Y is directly_closed holds
[:X,Y:] is directly_closed
let Y be Subset of T; ::_thesis: ( X is directly_closed & Y is directly_closed implies [:X,Y:] is directly_closed )
assume 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 ; :: according to WAYBEL11:def_2 ::_thesis: [:X,Y:] is directly_closed
let D be non empty directed Subset of [:S,T:]; :: according to WAYBEL11:def_2 ::_thesis: ( not D c= [:X,Y:] or "\/" (D,[:S,T:]) in [:X,Y:] )
assume A3: D c= [:X,Y:] ; ::_thesis: "\/" (D,[:S,T:]) in [:X,Y:]
 ( not proj2 D is empty & proj2 D is directed ) by YELLOW_3:21, YELLOW_3:22;
then A4: sup (proj2 D) in Y by A2, A3, FUNCT_5:11;
 ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A5: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
 ( not proj1 D is empty & proj1 D is directed ) by YELLOW_3:21, YELLOW_3:22;
then  sup (proj1 D) in X by A1, A3, FUNCT_5:11;
hence  "\/" (D,[:S,T:]) in [:X,Y:] by A4, A5, ZFMISC_1:87; ::_thesis: verum
end;

theorem :: YELLOW10:60
for S, T being non empty reflexive antisymmetric up-complete RelStr
for X being Subset of [:S,T:] st X is property(S) holds
( proj1 X is property(S) & proj2 X is property(S) )
proof
let S, T be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for X being Subset of [:S,T:] st X is property(S) holds
( proj1 X is property(S) & proj2 X is property(S) )
let X be Subset of [:S,T:]; ::_thesis: ( X is property(S) implies ( proj1 X is property(S) & proj2 X is property(S) ) )
assume A1: for D being non empty directed Subset of [:S,T:] st sup D in X holds
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 ) ) ; :: according to WAYBEL11:def_3 ::_thesis: ( proj1 X is property(S) & proj2 X is property(S) )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
hereby  :: according to WAYBEL11:def_3 ::_thesis: proj2 X is property(S)
let D be non empty directed Subset of S; ::_thesis: ( sup D in proj1 X implies ex z being M2( the carrier of S) st
( z in D & ( for x being Element of S st x in D & x >= z holds
x in proj1 X ) ) )
assume  sup D in proj1 X ; ::_thesis: ex z being M2( the carrier of S) st
( z in D & ( for x being Element of S st x in D & x >= z holds
x in proj1 X ) )
then consider t being set  such that
A3: [(sup D),t] in X by XTUPLE_0:def_12;
reconsider t = t as Element of T by A2, A3, ZFMISC_1:87;
reconsider t9 = {t} as non empty directed Subset of T by WAYBEL_0:5;
 ex_sup_of [:D,t9:],[:S,T:] by WAYBEL_0:75;
then  sup [:D,t9:] = [(sup (proj1 [:D,t9:])),(sup (proj2 [:D,t9:]))] by YELLOW_3:46
.= [(sup D),(sup (proj2 [:D,t9:]))] by FUNCT_5:9
.= [(sup D),(sup t9)] by FUNCT_5:9
.= [(sup D),t] by YELLOW_0:39 ;
then consider y being Element of [:S,T:] such that
A4: y in [:D,t9:] and
A5: for x being Element of [:S,T:] st x in [:D,t9:] & x >= y holds
x in X by A1, A3;
take z = y `1 ; ::_thesis: ( z in D & ( for x being Element of S st x in D & x >= z holds
x in proj1 X ) )
A6: y = [(y `1),(y `2)] by A2, MCART_1:21;
hence  z in D by A4, ZFMISC_1:87; ::_thesis: for x being Element of S st x in D & x >= z holds
x in proj1 X
A7: y `2 = t by A4, A6, ZFMISC_1:106;
let x be Element of S; ::_thesis: ( x in D & x >= z implies x in proj1 X )
assume  x in D ; ::_thesis: ( x >= z implies x in proj1 X )
then A8: [x,t] in [:D,t9:] by ZFMISC_1:106;
A9: y `2 <= y `2 ;
assume  x >= z ; ::_thesis: x in proj1 X
then  [x,t] >= y by A6, A7, A9, YELLOW_3:11;
then  [x,t] in X by A5, A8;
hence  x in proj1 X by XTUPLE_0:def_12; ::_thesis: verum
end;
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in proj2 X or ex b1 being M2( the carrier of T) st
( b1 in D & ( for b2 being M2( the carrier of T) holds
( not b2 in D or not b1 <= b2 or b2 in proj2 X ) ) ) )
assume  sup D in proj2 X ; ::_thesis: ex b1 being M2( the carrier of T) st
( b1 in D & ( for b2 being M2( the carrier of T) holds
( not b2 in D or not b1 <= b2 or b2 in proj2 X ) ) )
then consider s being set  such that
A10: [s,(sup D)] in X by XTUPLE_0:def_13;
reconsider s = s as Element of S by A2, A10, ZFMISC_1:87;
reconsider s9 = {s} as non empty directed Subset of S by WAYBEL_0:5;
 ex_sup_of [:s9,D:],[:S,T:] by WAYBEL_0:75;
then  sup [:s9,D:] = [(sup (proj1 [:s9,D:])),(sup (proj2 [:s9,D:]))] by YELLOW_3:46
.= [(sup s9),(sup (proj2 [:s9,D:]))] by FUNCT_5:9
.= [(sup s9),(sup D)] by FUNCT_5:9
.= [s,(sup D)] by YELLOW_0:39 ;
then consider y being Element of [:S,T:] such that
A11: y in [:s9,D:] and
A12: for x being Element of [:S,T:] st x in [:s9,D:] & x >= y holds
x in X by A1, A10;
take z = y `2 ; ::_thesis: ( z in D & ( for b1 being M2( the carrier of T) holds
( not b1 in D or not z <= b1 or b1 in proj2 X ) ) )
A13: y = [(y `1),(y `2)] by A2, MCART_1:21;
hence  z in D by A11, ZFMISC_1:87; ::_thesis: for b1 being M2( the carrier of T) holds
( not b1 in D or not z <= b1 or b1 in proj2 X )
A14: y `1 = s by A11, A13, ZFMISC_1:105;
let x be Element of T; ::_thesis: ( not x in D or not z <= x or x in proj2 X )
assume  x in D ; ::_thesis: ( not z <= x or x in proj2 X )
then A15: [s,x] in [:s9,D:] by ZFMISC_1:105;
A16: y `1 <= y `1 ;
assume  x >= z ; ::_thesis: x in proj2 X
then  [s,x] >= y by A13, A14, A16, YELLOW_3:11;
then  [s,x] in X by A12, A15;
hence  x in proj2 X by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem :: YELLOW10:61
for S, T being non empty up-complete Poset
for X being Subset of S
for Y being Subset of T st X is property(S) & Y is property(S) holds
[:X,Y:] is property(S)
proof
let S, T be non empty up-complete Poset; ::_thesis: for X being Subset of S
for Y being Subset of T st X is property(S) & Y is property(S) holds
[:X,Y:] is property(S)
let X be Subset of S; ::_thesis: for Y being Subset of T st X is property(S) & Y is property(S) holds
[:X,Y:] is property(S)
let Y be Subset of T; ::_thesis: ( X is property(S) & Y is property(S) implies [:X,Y:] is property(S) )
assume that
A1: for D being non empty directed Subset of S st sup D in X holds
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 holds
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 ) ) ; :: according to WAYBEL11:def_3 ::_thesis: [:X,Y:] is property(S)
let D be non empty directed Subset of [:S,T:]; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,[:S,T:]) in [:X,Y:] or ex b1 being M2( the carrier of [:S,T:]) st
( b1 in D & ( for b2 being M2( the carrier of [:S,T:]) holds
( not b2 in D or not b1 <= b2 or b2 in [:X,Y:] ) ) ) )
assume A3: sup D in [:X,Y:] ; ::_thesis: ex b1 being M2( the carrier of [:S,T:]) st
( b1 in D & ( for b2 being M2( the carrier of [:S,T:]) holds
( not b2 in D or not b1 <= b2 or b2 in [:X,Y:] ) ) )
 ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A4: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
then  ( not proj1 D is empty & proj1 D is directed & sup (proj1 D) in X ) by A3, YELLOW_3:21, YELLOW_3:22, ZFMISC_1:87;
then consider s being Element of S such that
A5: s in proj1 D and
A6: for x being Element of S st x in proj1 D & x >= s holds
x in X by A1;
consider s2 being set  such that
A7: [s,s2] in D by A5, XTUPLE_0:def_12;
 ( not proj2 D is empty & proj2 D is directed & sup (proj2 D) in Y ) by A3, A4, YELLOW_3:21, YELLOW_3:22, ZFMISC_1:87;
then 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;
consider t1 being set  such that
A10: [t1,t] in D by A8, XTUPLE_0:def_13;
A11: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then reconsider s2 = s2 as Element of T by A7, ZFMISC_1:87;
reconsider t1 = t1 as Element of S by A11, A10, ZFMISC_1:87;
consider z being Element of [:S,T:] such that
A12: z in D and
A13: [s,s2] <= z and
A14: [t1,t] <= z by A7, A10, WAYBEL_0:def_1;
A15: z = [(z `1),(z `2)] by A11, MCART_1:21;
then A16: t <= z `2 by A14, YELLOW_3:11;
take  z ; ::_thesis: ( z in D & ( for b1 being M2( the carrier of [:S,T:]) holds
( not b1 in D or not z <= b1 or b1 in [:X,Y:] ) ) )
thus  z in D by A12; ::_thesis: for b1 being M2( the carrier of [:S,T:]) holds
( not b1 in D or not z <= b1 or b1 in [:X,Y:] )
let x be Element of [:S,T:]; ::_thesis: ( not x in D or not z <= x or x in [:X,Y:] )
assume A17: x in D ; ::_thesis: ( not z <= x or x in [:X,Y:] )
assume A18: x >= z ; ::_thesis: x in [:X,Y:]
then A19: x `2 >= z `2 by YELLOW_3:12;
A20: x = [(x `1),(x `2)] by A11, MCART_1:21;
then  x `2 in proj2 D by A17, XTUPLE_0:def_13;
then A21: x `2 in Y by A9, A19, A16, ORDERS_2:3;
A22: s <= z `1 by A13, A15, YELLOW_3:11;
A23: x `1 >= z `1 by A18, YELLOW_3:12;
 x `1 in proj1 D by A17, A20, XTUPLE_0:def_12;
then  x `1 in X by A6, A23, A22, ORDERS_2:3;
hence  x in [:X,Y:] by A20, A21, ZFMISC_1:87; ::_thesis: verum
end;

begin

theorem Th62: :: YELLOW10:62
for S, T being non empty reflexive RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & S is /\-complete holds
T is /\-complete
proof
let S, T be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) & S is /\-complete implies T is /\-complete )
assume that
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel 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 ) ) ; :: according to WAYBEL_0:def_40 ::_thesis: T is /\-complete
let X be non empty Subset of T; :: according to WAYBEL_0:def_40 ::_thesis: ex b1 being M2( the carrier of T) st
( b1 is_<=_than X & ( for b2 being M2( the carrier of T) holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
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 A1, A2;
reconsider z = x as Element of T by A1;
take  z ; ::_thesis: ( z is_<=_than X & ( for b1 being M2( the carrier of T) holds
( not b1 is_<=_than X or b1 <= z ) ) )
thus  z is_<=_than X by A1, A3, YELLOW_0:2; ::_thesis: for b1 being M2( the carrier of T) holds
( not b1 is_<=_than X or b1 <= z )
let y be Element of T; ::_thesis: ( not y is_<=_than X or y <= z )
reconsider s = y as Element of S by A1;
assume  y is_<=_than X ; ::_thesis: y <= z
then  x >= s by A1, A4, YELLOW_0:2;
hence  y <= z by A1, YELLOW_0:1; ::_thesis: verum
end;

registration
let S be non empty reflexive /\-complete RelStr ;
cluster RelStr(# the carrier of S, the InternalRel of S #) ->  /\-complete ;
coherence
 RelStr(# the carrier of S, the InternalRel of S #) is /\-complete by Th62;
end;

registration
let S, T be non empty reflexive /\-complete RelStr ;
cluster[:S,T:] ->  /\-complete ;
coherence
 [:S,T:] is /\-complete
proof
let X be non empty Subset of [:S,T:]; :: according to WAYBEL_0:def_40 ::_thesis: ex b1 being M2( the carrier of [:S,T:]) st
( b1 is_<=_than X & ( for b2 being M2( the carrier of [:S,T:]) holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
 not proj1 X is 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;
 not proj2 X is 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] ; ::_thesis: ( [s,t] is_<=_than X & ( for b1 being M2( the carrier of [:S,T:]) holds
( not b1 is_<=_than X or b1 <= [s,t] ) ) )
thus  [s,t] is_<=_than X by A1, A3, YELLOW_3:34; ::_thesis: for b1 being M2( the carrier of [:S,T:]) holds
( not b1 is_<=_than X or b1 <= [s,t] )
let y be Element of [:S,T:]; ::_thesis: ( not y is_<=_than X or y <= [s,t] )
 the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A5: y = [(y `1),(y `2)] by MCART_1:21;
assume A6: y is_<=_than X ; ::_thesis: y <= [s,t]
then  y `2 is_<=_than proj2 X by A5, YELLOW_3:34;
then A7: t >= y `2 by A4;
 y `1 is_<=_than proj1 X by A5, A6, YELLOW_3:34;
then  s >= y `1 by A2;
hence  y <= [s,t] by A5, A7, YELLOW_3:11; ::_thesis: verum
end;
end;

theorem :: YELLOW10:63
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 ; ::_thesis: ( [:S,T:] is /\-complete implies ( S is /\-complete & T is /\-complete ) )
assume 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 ) ) ; :: according to WAYBEL_0:def_40 ::_thesis: ( S is /\-complete & T is /\-complete )
A2: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
thus  S is /\-complete ::_thesis: T is /\-complete
proof
set t = the Element of T;
let X be non empty Subset of S; :: according to WAYBEL_0:def_40 ::_thesis: ex b1 being M2( the carrier of S) st
( b1 is_<=_than X & ( for b2 being M2( the carrier of S) holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
consider x being Element of [:S,T:] such that
A3: x is_<=_than [:X,{ the Element of T}:] and
A4: for y being Element of [:S,T:] st y is_<=_than [:X,{ the Element of T}:] holds
x >= y by A1;
take  x `1 ; ::_thesis: ( x `1 is_<=_than X & ( for b1 being M2( the carrier of S) holds
( not b1 is_<=_than X or b1 <= x `1 ) ) )
A5: x = [(x `1),(x `2)] by A2, MCART_1:21;
hence  x `1 is_<=_than X by A3, YELLOW_3:32; ::_thesis: for b1 being M2( the carrier of S) holds
( not b1 is_<=_than X or b1 <= x `1 )
 the Element of T <= the Element of T ;
then A6: the Element of T is_<=_than { the Element of T} by YELLOW_0:7;
let y be Element of S; ::_thesis: ( not y is_<=_than X or y <= x `1 )
assume  y is_<=_than X ; ::_thesis: y <= x `1
then  x >= [y, the Element of T] by A4, A6, YELLOW_3:33;
hence  y <= x `1 by A5, YELLOW_3:11; ::_thesis: verum
end;
set s = the Element of S;
let X be non empty Subset of T; :: according to WAYBEL_0:def_40 ::_thesis: ex b1 being M2( the carrier of T) st
( b1 is_<=_than X & ( for b2 being M2( the carrier of T) holds
( not b2 is_<=_than X or b2 <= b1 ) ) )
consider x being Element of [:S,T:] such that
A7: x is_<=_than [:{ the Element of S},X:] and
A8: for y being Element of [:S,T:] st y is_<=_than [:{ the Element of S},X:] holds
x >= y by A1;
take  x `2 ; ::_thesis: ( x `2 is_<=_than X & ( for b1 being M2( the carrier of T) holds
( not b1 is_<=_than X or b1 <= x `2 ) ) )
A9: x = [(x `1),(x `2)] by A2, MCART_1:21;
hence  x `2 is_<=_than X by A7, YELLOW_3:32; ::_thesis: for b1 being M2( the carrier of T) holds
( not b1 is_<=_than X or b1 <= x `2 )
 the Element of S <= the Element of S ;
then A10: the Element of S is_<=_than { the Element of S} by YELLOW_0:7;
let y be Element of T; ::_thesis: ( not y is_<=_than X or y <= x `2 )
assume  y is_<=_than X ; ::_thesis: y <= x `2
then  x >= [ the Element of S,y] by A8, A10, YELLOW_3:33;
hence  y <= x `2 by A9, YELLOW_3:11; ::_thesis: verum
end;

registration
let S, T be non empty antisymmetric bounded complemented with_suprema with_infima RelStr ;
cluster[:S,T:] ->  complemented ;
coherence
 [:S,T:] is complemented
proof
let x be Element of [:S,T:]; :: according to WAYBEL_1:def_24 ::_thesis: ex b1 being M2( the carrier of [:S,T:]) st b1 is_a_complement_of x
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] ; ::_thesis: [s,t] is_a_complement_of x
 ( [s,t] `1 = s & [s,t] `2 = t ) ;
hence  [s,t] is_a_complement_of x by A1, A2, Th17; ::_thesis: verum
end;
end;

theorem :: YELLOW10:64
for S, T being antisymmetric bounded with_suprema with_infima RelStr st [:S,T:] is complemented holds
( S is complemented & T is complemented )
proof
let S, T be antisymmetric bounded with_suprema with_infima RelStr ; ::_thesis: ( [:S,T:] is complemented implies ( S is complemented & T is complemented ) )
set s = the Element of S;
assume A1: for x being Element of [:S,T:] ex y being Element of [:S,T:] st y is_a_complement_of x ; :: according to WAYBEL_1:def_24 ::_thesis: ( S is complemented & T is complemented )
thus  S is complemented ::_thesis: T is complemented
proof
set t = the Element of T;
let s be Element of S; :: according to WAYBEL_1:def_24 ::_thesis: ex b1 being M2( the carrier of S) st b1 is_a_complement_of s
consider y being Element of [:S,T:] such that
A2: y is_a_complement_of [s, the Element of T] by A1;
take  y `1 ; ::_thesis: y `1 is_a_complement_of s
 [s, the Element of T] `1 = s ;
hence  y `1 is_a_complement_of s by A2, Th17; ::_thesis: verum
end;
let t be Element of T; :: according to WAYBEL_1:def_24 ::_thesis: ex b1 being M2( the carrier of T) st b1 is_a_complement_of t
consider y being Element of [:S,T:] such that
A3: y is_a_complement_of [ the Element of S,t] by A1;
take  y `2 ; ::_thesis: y `2 is_a_complement_of t
 [ the Element of S,t] `2 = t ;
hence  y `2 is_a_complement_of t by A3, Th17; ::_thesis: verum
end;

registration
let S, T be non empty antisymmetric distributive with_suprema with_infima RelStr ;
cluster[:S,T:] ->  distributive ;
coherence
 [:S,T:] is distributive
proof
let x, y, z be Element of [:S,T:]; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
A2: (x "/\" (y "\/" z)) `2 = (x `2) "/\" ((y "\/" z) `2) by Th13
.= (x `2) "/\" ((y `2) "\/" (z `2)) by Th14
.= ((x `2) "/\" (y `2)) "\/" ((x `2) "/\" (z `2)) by WAYBEL_1:def_3
.= ((x "/\" y) `2) "\/" ((x `2) "/\" (z `2)) by Th13
.= ((x "/\" y) `2) "\/" ((x "/\" z) `2) by Th13
.= ((x "/\" y) "\/" (x "/\" z)) `2 by Th14 ;
(x "/\" (y "\/" z)) `1 = (x `1) "/\" ((y "\/" z) `1) by Th13
.= (x `1) "/\" ((y `1) "\/" (z `1)) by Th14
.= ((x `1) "/\" (y `1)) "\/" ((x `1) "/\" (z `1)) by WAYBEL_1:def_3
.= ((x "/\" y) `1) "\/" ((x `1) "/\" (z `1)) by Th13
.= ((x "/\" y) `1) "\/" ((x "/\" z) `1) by Th13
.= ((x "/\" y) "\/" (x "/\" z)) `1 by Th14 ;
hence  x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A1, A2, DOMAIN_1:2; ::_thesis: verum
end;
end;

theorem :: YELLOW10:65
for S being antisymmetric with_suprema with_infima RelStr
for T being reflexive antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
S is distributive
proof
let S be antisymmetric with_suprema with_infima RelStr ; ::_thesis: for T being reflexive antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
S is distributive
let T be reflexive antisymmetric with_suprema with_infima RelStr ; ::_thesis: ( [:S,T:] is distributive implies S is distributive )
assume A1: for x, y, z being Element of [:S,T:] holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; :: according to WAYBEL_1:def_3 ::_thesis: S is distributive
set t = the Element of T;
let x, y, z be Element of S; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A2: the Element of T "/\" the Element of T = the Element of T by YELLOW_0:25;
 the Element of T <= the Element of T ;
then A3: the Element of T "\/" the Element of T = the Element of T by YELLOW_0:24;
thus x "/\" (y "\/" z) = [(x "/\" (y "\/" z)), the Element of T] `1
.= ([x, the Element of T] "/\" [(y "\/" z), the Element of T]) `1 by A2, Th15
.= ([x, the Element of T] "/\" ([y, the Element of T] "\/" [z, the Element of T])) `1 by A3, Th16
.= (([x, the Element of T] "/\" [y, the Element of T]) "\/" ([x, the Element of T] "/\" [z, the Element of T])) `1 by A1
.= ([(x "/\" y), the Element of T] "\/" ([x, the Element of T] "/\" [z, the Element of T])) `1 by A2, Th15
.= ([(x "/\" y), the Element of T] "\/" [(x "/\" z), the Element of T]) `1 by A2, Th15
.= [((x "/\" y) "\/" (x "/\" z)), the Element of T] `1 by A3, Th16
.= (x "/\" y) "\/" (x "/\" z) ; ::_thesis: verum
end;

theorem :: YELLOW10:66
for S being reflexive antisymmetric with_suprema with_infima RelStr
for T being antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
T is distributive
proof
let S be reflexive antisymmetric with_suprema with_infima RelStr ; ::_thesis: for T being antisymmetric with_suprema with_infima RelStr st [:S,T:] is distributive holds
T is distributive
let T be antisymmetric with_suprema with_infima RelStr ; ::_thesis: ( [:S,T:] is distributive implies T is distributive )
assume A1: for x, y, z being Element of [:S,T:] holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) ; :: according to WAYBEL_1:def_3 ::_thesis: T is distributive
set s = the Element of S;
let x, y, z be Element of T; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A2: the Element of S "/\" the Element of S = the Element of S by YELLOW_0:25;
 the Element of S <= the Element of S ;
then A3: the Element of S "\/" the Element of S = the Element of S by YELLOW_0:24;
thus x "/\" (y "\/" z) = [ the Element of S,(x "/\" (y "\/" z))] `2
.= ([ the Element of S,x] "/\" [ the Element of S,(y "\/" z)]) `2 by A2, Th15
.= ([ the Element of S,x] "/\" ([ the Element of S,y] "\/" [ the Element of S,z])) `2 by A3, Th16
.= (([ the Element of S,x] "/\" [ the Element of S,y]) "\/" ([ the Element of S,x] "/\" [ the Element of S,z])) `2 by A1
.= ([ the Element of S,(x "/\" y)] "\/" ([ the Element of S,x] "/\" [ the Element of S,z])) `2 by A2, Th15
.= ([ the Element of S,(x "/\" y)] "\/" [ the Element of S,(x "/\" z)]) `2 by A2, Th15
.= [ the Element of S,((x "/\" y) "\/" (x "/\" z))] `2 by A3, Th16
.= (x "/\" y) "\/" (x "/\" z) ; ::_thesis: verum
end;

registration
let S, T be meet-continuous Semilattice;
cluster[:S,T:] ->  satisfying_MC ;
coherence
 [:S,T:] is satisfying_MC
proof
let x be Element of [:S,T:]; :: according to WAYBEL_2:def_6 ::_thesis: for b1 being M2( bool the carrier of [:S,T:]) holds x "/\" ("\/" (b1,[:S,T:])) = "\/" (({x} "/\" b1),[:S,T:])
let D be non empty directed Subset of [:S,T:]; ::_thesis: x "/\" ("\/" (D,[:S,T:])) = "\/" (({x} "/\" D),[:S,T:])
A1: ( not proj1 D is empty & proj1 D is directed ) by YELLOW_3:21, YELLOW_3:22;
reconsider x9 = {x} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
A2: ( not proj2 D is empty & proj2 D is directed ) by YELLOW_3:21, YELLOW_3:22;
A3: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
then A4: x = [(x `1),(x `2)] by MCART_1:21;
 ex_sup_of x9 "/\" D,[:S,T:] by WAYBEL_0:75;
then A5: sup ({x} "/\" D) = [(sup (proj1 ({x} "/\" D))),(sup (proj2 ({x} "/\" D)))] by YELLOW_3:46;
 ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A6: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
A7: (x "/\" (sup D)) `2 = (x `2) "/\" ((sup D) `2) by Th13
.= (x `2) "/\" (sup (proj2 D)) by A6, MCART_1:7
.= sup ({(x `2)} "/\" (proj2 D)) by A2, WAYBEL_2:def_6
.= sup ((proj2 {x}) "/\" (proj2 D)) by A4, FUNCT_5:12
.= sup (proj2 ({x} "/\" D)) by Th24
.= (sup ({x} "/\" D)) `2 by A5, MCART_1:7 ;
(x "/\" (sup D)) `1 = (x `1) "/\" ((sup D) `1) by Th13
.= (x `1) "/\" (sup (proj1 D)) by A6, MCART_1:7
.= sup ({(x `1)} "/\" (proj1 D)) by A1, WAYBEL_2:def_6
.= sup ((proj1 {x}) "/\" (proj1 D)) by A4, FUNCT_5:12
.= sup (proj1 ({x} "/\" D)) by Th24
.= (sup ({x} "/\" D)) `1 by A5, MCART_1:7 ;
hence  x "/\" (sup D) = sup ({x} "/\" D) by A3, A7, DOMAIN_1:2; ::_thesis: verum
end;
end;

theorem :: YELLOW10:67
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; ::_thesis: ( [:S,T:] is meet-continuous implies ( S is meet-continuous & T is meet-continuous ) )
assume that
A1: [:S,T:] is up-complete and
A2: for x being Element of [:S,T:]
for D being non empty directed Subset of [:S,T:] holds x "/\" (sup D) = sup ({x} "/\" D) ; :: according to WAYBEL_2:def_6,WAYBEL_2:def_7 ::_thesis: ( S is meet-continuous & T is meet-continuous )
hereby  :: according to WAYBEL_2:def_6,WAYBEL_2:def_7 ::_thesis: T is meet-continuous
thus  S is up-complete by A1, WAYBEL_2:11; ::_thesis: for s being Element of S
for D being non empty directed Subset of S holds sup ({s} "/\" D) = s "/\" (sup D)
set t = the Element of T;
let s be Element of S; ::_thesis: for D being non empty directed Subset of S holds sup ({s} "/\" D) = s "/\" (sup D)
let D be non empty directed Subset of S; ::_thesis: sup ({s} "/\" D) = s "/\" (sup D)
reconsider t9 = { the Element of T} as non empty directed Subset of T by WAYBEL_0:5;
reconsider ST = {[s, the Element of T]} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
 ex_sup_of [:D,t9:],[:S,T:] by A1, WAYBEL_0:75;
then A3: sup [:D,t9:] = [(sup (proj1 [:D,t9:])),(sup (proj2 [:D,t9:]))] by YELLOW_3:46;
 ex_sup_of ST "/\" [:D,t9:],[:S,T:] by A1, WAYBEL_0:75;
then A4: sup ({[s, the Element of T]} "/\" [:D,t9:]) = [(sup (proj1 ({[s, the Element of T]} "/\" [:D,t9:]))),(sup (proj2 ({[s, the Element of T]} "/\" [:D,t9:])))] by YELLOW_3:46;
thus  sup ({s} "/\" D) = sup ((proj1 {[s, the Element of T]}) "/\" D) by FUNCT_5:12
.= sup ((proj1 {[s, the Element of T]}) "/\" (proj1 [:D,t9:])) by FUNCT_5:9
.= sup (proj1 ({[s, the Element of T]} "/\" [:D,t9:])) by Th24
.= (sup ({[s, the Element of T]} "/\" [:D,t9:])) `1 by A4, MCART_1:7
.= ([s, the Element of T] "/\" (sup [:D,t9:])) `1 by A2
.= ([s, the Element of T] `1) "/\" ((sup [:D,t9:]) `1) by Th13
.= s "/\" ((sup [:D,t9:]) `1)
.= s "/\" (sup (proj1 [:D,t9:])) by A3, MCART_1:7
.= s "/\" (sup D) by FUNCT_5:9 ; ::_thesis: verum
end;
thus  T is up-complete by A1, WAYBEL_2:11; :: according to WAYBEL_2:def_7 ::_thesis: T is satisfying_MC
set s = the Element of S;
let t be Element of T; :: according to WAYBEL_2:def_6 ::_thesis: for b1 being M2( bool the carrier of T) holds t "/\" ("\/" (b1,T)) = "\/" (({t} "/\" b1),T)
let D be non empty directed Subset of T; ::_thesis: t "/\" ("\/" (D,T)) = "\/" (({t} "/\" D),T)
reconsider s9 = { the Element of S} as non empty directed Subset of S by WAYBEL_0:5;
 ex_sup_of [:s9,D:],[:S,T:] by A1, WAYBEL_0:75;
then A5: sup [:s9,D:] = [(sup (proj1 [:s9,D:])),(sup (proj2 [:s9,D:]))] by YELLOW_3:46;
reconsider ST = {[ the Element of S,t]} as non empty directed Subset of [:S,T:] by WAYBEL_0:5;
 ex_sup_of ST "/\" [:s9,D:],[:S,T:] by A1, WAYBEL_0:75;
then A6: sup ({[ the Element of S,t]} "/\" [:s9,D:]) = [(sup (proj1 ({[ the Element of S,t]} "/\" [:s9,D:]))),(sup (proj2 ({[ the Element of S,t]} "/\" [:s9,D:])))] by YELLOW_3:46;
thus  sup ({t} "/\" D) = sup ((proj2 {[ the Element of S,t]}) "/\" D) by FUNCT_5:12
.= sup ((proj2 {[ the Element of S,t]}) "/\" (proj2 [:s9,D:])) by FUNCT_5:9
.= sup (proj2 ({[ the Element of S,t]} "/\" [:s9,D:])) by Th24
.= (sup ({[ the Element of S,t]} "/\" [:s9,D:])) `2 by A6, MCART_1:7
.= ([ the Element of S,t] "/\" (sup [:s9,D:])) `2 by A2
.= ([ the Element of S,t] `2) "/\" ((sup [:s9,D:]) `2) by Th13
.= t "/\" ((sup [:s9,D:]) `2)
.= t "/\" (sup (proj2 [:s9,D:])) by A5, MCART_1:7
.= t "/\" (sup D) by FUNCT_5:9 ; ::_thesis: verum
end;

registration
let S, T be non empty up-complete /\-complete satisfying_axiom_of_approximation Poset;
cluster[:S,T:] ->  satisfying_axiom_of_approximation ;
coherence
 [:S,T:] is satisfying_axiom_of_approximation
proof
let x be Element of [:S,T:]; :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),[:S,T:])
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
 ex_sup_of waybelow x,[:S,T:] by WAYBEL_0:75;
then A2: sup (waybelow x) = [(sup (proj1 (waybelow x))),(sup (proj2 (waybelow x)))] by YELLOW_3:46;
then A3: (sup (waybelow x)) `2 = sup (proj2 (waybelow x)) by MCART_1:7
.= sup (waybelow (x `2)) by Th47
.= x `2 by WAYBEL_3:def_5 ;
(sup (waybelow x)) `1 = sup (proj1 (waybelow x)) by A2, MCART_1:7
.= sup (waybelow (x `1)) by Th46
.= x `1 by WAYBEL_3:def_5 ;
hence  x = "\/" ((waybelow x),[:S,T:]) by A1, A3, DOMAIN_1:2; ::_thesis: verum
end;
end;

registration
let S, T be non empty /\-complete continuous Poset;
cluster[:S,T:] ->  continuous ;
coherence
 [:S,T:] is continuous
proof
thus  for x being Element of [:S,T:] holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_of_approximation )
thus  ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_of_approximation ) ; ::_thesis: verum
end;
end;

theorem :: YELLOW10:68
for S, T being non empty lower-bounded up-complete Poset st [:S,T:] is continuous holds
( S is continuous & T is continuous )
proof
let S, T be non empty lower-bounded up-complete Poset; ::_thesis: ( [:S,T:] is continuous implies ( S is continuous & T is continuous ) )
assume that
A1: for x being Element of [:S,T:] holds
( not waybelow x is empty & waybelow x is directed ) and
A2: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_of_approximation ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( S is continuous & T is continuous )
hereby  :: according to WAYBEL_3:def_6 ::_thesis: T is continuous
hereby  ::_thesis: ( S is up-complete & S is satisfying_axiom_of_approximation )
set t = the Element of T;
let s be Element of S; ::_thesis: ( not waybelow s is empty & waybelow s is directed )
A3: waybelow [s, the Element of T] is directed by A1;
 ( [:(waybelow s),(waybelow the Element of T):] = waybelow [s, the Element of T] & proj1 [:(waybelow s),(waybelow the Element of T):] = waybelow s ) by Th44, FUNCT_5:9;
hence  ( not waybelow s is empty & waybelow s is directed ) by A3, YELLOW_3:22; ::_thesis: verum
end;
thus  S is up-complete ; ::_thesis: S is satisfying_axiom_of_approximation
thus  S is satisfying_axiom_of_approximation ::_thesis: verum
proof
set t = the Element of T;
let s be Element of S; :: according to WAYBEL_3:def_5 ::_thesis: s = "\/" ((waybelow s),S)
 waybelow [s, the Element of T] is directed by A1;
then  ex_sup_of waybelow [s, the Element of T],[:S,T:] by WAYBEL_0:75;
then A4: sup (waybelow [s, the Element of T]) = [(sup (proj1 (waybelow [s, the Element of T]))),(sup (proj2 (waybelow [s, the Element of T])))] by Th5;
thus s = [s, the Element of T] `1
.= (sup (waybelow [s, the Element of T])) `1 by A2, WAYBEL_3:def_5
.= sup (proj1 (waybelow [s, the Element of T])) by A4, MCART_1:7
.= sup (waybelow ([s, the Element of T] `1)) by Th46
.= sup (waybelow s) ; ::_thesis: verum
end;
end;
hereby  :: according to WAYBEL_3:def_6 ::_thesis: ( T is up-complete & T is satisfying_axiom_of_approximation )
set s = the Element of S;
let t be Element of T; ::_thesis: ( not waybelow t is empty & waybelow t is directed )
A5: waybelow [ the Element of S,t] is directed by A1;
 ( [:(waybelow the Element of S),(waybelow t):] = waybelow [ the Element of S,t] & proj2 [:(waybelow the Element of S),(waybelow t):] = waybelow t ) by Th44, FUNCT_5:9;
hence  ( not waybelow t is empty & waybelow t is directed ) by A5, YELLOW_3:22; ::_thesis: verum
end;
set s = the Element of S;
thus  T is up-complete ; ::_thesis: T is satisfying_axiom_of_approximation
let t be Element of T; :: according to WAYBEL_3:def_5 ::_thesis: t = "\/" ((waybelow t),T)
now__::_thesis:_for_x_being_Element_of_[:S,T:]_holds_ex_sup_of_waybelow_x,[:S,T:]
let x be Element of [:S,T:]; ::_thesis: ex_sup_of waybelow x,[:S,T:]
 ( not waybelow x is empty & waybelow x is directed ) by A1;
hence  ex_sup_of waybelow x,[:S,T:] by WAYBEL_0:75; ::_thesis: verum
end;
then A6: sup (waybelow [ the Element of S,t]) = [(sup (proj1 (waybelow [ the Element of S,t]))),(sup (proj2 (waybelow [ the Element of S,t])))] by Th5;
thus t = [ the Element of S,t] `2
.= (sup (waybelow [ the Element of S,t])) `2 by A2, WAYBEL_3:def_5
.= sup (proj2 (waybelow [ the Element of S,t])) by A6, MCART_1:7
.= sup (waybelow ([ the Element of S,t] `2)) by Th47
.= sup (waybelow t) ; ::_thesis: verum
end;

registration
let S, T be lower-bounded up-complete satisfying_axiom_K sup-Semilattice;
cluster[:S,T:] ->  satisfying_axiom_K ;
coherence
 [:S,T:] is satisfying_axiom_K
proof
let x be Element of [:S,T:]; :: according to WAYBEL_8:def_3 ::_thesis: x = "\/" ((compactbelow x),[:S,T:])
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def_2;
A2: sup (compactbelow x) = [(sup (proj1 (compactbelow x))),(sup (proj2 (compactbelow x)))] by YELLOW_3:46;
then A3: (sup (compactbelow x)) `2 = sup (proj2 (compactbelow x)) by MCART_1:7
.= sup (compactbelow (x `2)) by Th53
.= x `2 by WAYBEL_8:def_3 ;
(sup (compactbelow x)) `1 = sup (proj1 (compactbelow x)) by A2, MCART_1:7
.= sup (compactbelow (x `1)) by Th52
.= x `1 by WAYBEL_8:def_3 ;
hence  x = "\/" ((compactbelow x),[:S,T:]) by A1, A3, DOMAIN_1:2; ::_thesis: verum
end;
end;

registration
let S, T be lower-bounded complete algebraic sup-Semilattice;
cluster[:S,T:] ->  algebraic ;
coherence
 [:S,T:] is algebraic
proof
thus  for x being Element of [:S,T:] holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def_4 ::_thesis: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_K )
thus  ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_K ) ; ::_thesis: verum
end;
end;

theorem Th69: :: YELLOW10:69
for S, T being non empty lower-bounded Poset st [:S,T:] is algebraic holds
( S is algebraic & T is algebraic )
proof
let S, T be non empty lower-bounded Poset; ::_thesis: ( [:S,T:] is algebraic implies ( S is algebraic & T is algebraic ) )
assume that
A1: for x being Element of [:S,T:] holds
( not compactbelow x is empty & compactbelow x is directed ) and
A2: ( [:S,T:] is up-complete & [:S,T:] is satisfying_axiom_K ) ; :: according to WAYBEL_8:def_4 ::_thesis: ( S is algebraic & T is algebraic )
A3: ( S is up-complete & T is up-complete ) by A2, WAYBEL_2:11;
hereby  :: according to WAYBEL_8:def_4 ::_thesis: T is algebraic
hereby  ::_thesis: ( S is up-complete & S is satisfying_axiom_K )
set t = the Element of T;
let s be Element of S; ::_thesis: ( not compactbelow s is empty & compactbelow s is directed )
A4: compactbelow [s, the Element of T] is directed by A1;
 ( [:(compactbelow s),(compactbelow the Element of T):] = compactbelow [s, the Element of T] & proj1 [:(compactbelow s),(compactbelow the Element of T):] = compactbelow s ) by A3, Th50, FUNCT_5:9;
hence  ( not compactbelow s is empty & compactbelow s is directed ) by A4, YELLOW_3:22; ::_thesis: verum
end;
thus  S is up-complete by A2, WAYBEL_2:11; ::_thesis: S is satisfying_axiom_K
thus  S is satisfying_axiom_K ::_thesis: verum
proof
set t = the Element of T;
let s be Element of S; :: according to WAYBEL_8:def_3 ::_thesis: s = "\/" ((compactbelow s),S)
 ( not compactbelow [s, the Element of T] is empty & compactbelow [s, the Element of T] is directed ) by A1;
then  ex_sup_of compactbelow [s, the Element of T],[:S,T:] by A2, WAYBEL_0:75;
then A5: sup (compactbelow [s, the Element of T]) = [(sup (proj1 (compactbelow [s, the Element of T]))),(sup (proj2 (compactbelow [s, the Element of T])))] by Th5;
thus s = [s, the Element of T] `1
.= (sup (compactbelow [s, the Element of T])) `1 by A2, WAYBEL_8:def_3
.= sup (proj1 (compactbelow [s, the Element of T])) by A5, MCART_1:7
.= sup (compactbelow ([s, the Element of T] `1)) by A3, Th52
.= sup (compactbelow s) ; ::_thesis: verum
end;
end;
set s = the Element of S;
hereby  :: according to WAYBEL_8:def_4 ::_thesis: ( T is up-complete & T is satisfying_axiom_K )
set s = the Element of S;
let t be Element of T; ::_thesis: ( not compactbelow t is empty & compactbelow t is directed )
A6: compactbelow [ the Element of S,t] is directed by A1;
 ( [:(compactbelow the Element of S),(compactbelow t):] = compactbelow [ the Element of S,t] & proj2 [:(compactbelow the Element of S),(compactbelow t):] = compactbelow t ) by A3, Th50, FUNCT_5:9;
hence  ( not compactbelow t is empty & compactbelow t is directed ) by A6, YELLOW_3:22; ::_thesis: verum
end;
thus  T is up-complete by A2, WAYBEL_2:11; ::_thesis: T is satisfying_axiom_K
let t be Element of T; :: according to WAYBEL_8:def_3 ::_thesis: t = "\/" ((compactbelow t),T)
 ( not compactbelow [ the Element of S,t] is empty & compactbelow [ the Element of S,t] is directed ) by A1;
then  ex_sup_of compactbelow [ the Element of S,t],[:S,T:] by A2, WAYBEL_0:75;
then A7: sup (compactbelow [ the Element of S,t]) = [(sup (proj1 (compactbelow [ the Element of S,t]))),(sup (proj2 (compactbelow [ the Element of S,t])))] by Th5;
thus t = [ the Element of S,t] `2
.= (sup (compactbelow [ the Element of S,t])) `2 by A2, WAYBEL_8:def_3
.= sup (proj2 (compactbelow [ the Element of S,t])) by A7, MCART_1:7
.= sup (compactbelow ([ the Element of S,t] `2)) by A3, Th53
.= sup (compactbelow t) ; ::_thesis: verum
end;

registration
let S, T be lower-bounded arithmetic LATTICE;
cluster[:S,T:] ->  arithmetic ;
coherence
 [:S,T:] is arithmetic
proof
set C = CompactSublatt [:S,T:];
thus  [:S,T:] is algebraic ; :: according to WAYBEL_8:def_5 ::_thesis: CompactSublatt [:S,T:] is meet-inheriting
let x, y be Element of [:S,T:]; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (CompactSublatt [:S,T:]) or not y in the carrier of (CompactSublatt [:S,T:]) or not ex_inf_of {x,y},[:S,T:] or "/\" ({x,y},[:S,T:]) in the carrier of (CompactSublatt [:S,T:]) )
assume that
A1: x in the carrier of (CompactSublatt [:S,T:]) and
A2: y in the carrier of (CompactSublatt [:S,T:]) and
 ex_inf_of {x,y},[:S,T:] ; ::_thesis: "/\" ({x,y},[:S,T:]) in the carrier of (CompactSublatt [:S,T:])
A3: x is compact by A1, WAYBEL_8:def_1;
then  x `1 is compact by Th22;
then A4: x `1 in the carrier of (CompactSublatt S) by WAYBEL_8:def_1;
A5: y is compact by A2, WAYBEL_8:def_1;
then  y `1 is compact by Th22;
then A6: y `1 in the carrier of (CompactSublatt S) by WAYBEL_8:def_1;
 x `2 is compact by A3, Th22;
then A7: x `2 in the carrier of (CompactSublatt T) by WAYBEL_8:def_1;
 y `2 is compact by A5, Th22;
then A8: y `2 in the carrier of (CompactSublatt T) by WAYBEL_8:def_1;
 ( CompactSublatt T is meet-inheriting & ex_inf_of {(x `2),(y `2)},T ) by WAYBEL_8:def_5, YELLOW_0:21;
then  inf {(x `2),(y `2)} in the carrier of (CompactSublatt T) by A7, A8, YELLOW_0:def_16;
then  (x `2) "/\" (y `2) in the carrier of (CompactSublatt T) by YELLOW_0:40;
then  (x `2) "/\" (y `2) is compact by WAYBEL_8:def_1;
then A9: (x "/\" y) `2 is compact by Th13;
 ( CompactSublatt S is meet-inheriting & ex_inf_of {(x `1),(y `1)},S ) by WAYBEL_8:def_5, YELLOW_0:21;
then  inf {(x `1),(y `1)} in the carrier of (CompactSublatt S) by A4, A6, YELLOW_0:def_16;
then  (x `1) "/\" (y `1) in the carrier of (CompactSublatt S) by YELLOW_0:40;
then  (x `1) "/\" (y `1) is compact by WAYBEL_8:def_1;
then  (x "/\" y) `1 is compact by Th13;
then  x "/\" y is compact by A9, Th23;
then  inf {x,y} is compact by YELLOW_0:40;
hence  "/\" ({x,y},[:S,T:]) in the carrier of (CompactSublatt [:S,T:]) by WAYBEL_8:def_1; ::_thesis: verum
end;
end;

theorem :: YELLOW10:70
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; ::_thesis: ( [:S,T:] is arithmetic implies ( S is arithmetic & T is arithmetic ) )
assume that
A1: [:S,T:] is algebraic and
A2: CompactSublatt [:S,T:] is meet-inheriting ; :: according to WAYBEL_8:def_5 ::_thesis: ( S is arithmetic & T is arithmetic )
A3: ( S is up-complete & T is up-complete ) by A1, WAYBEL_2:11;
hereby  :: according to YELLOW_0:def_16,WAYBEL_8:def_5 ::_thesis: T is arithmetic
thus  S is algebraic by A1, Th69; ::_thesis: for x, y being Element of S st x in the carrier of (CompactSublatt S) & y in the carrier of (CompactSublatt S) & ex_inf_of {x,y},S holds
inf {x,y} in the carrier of (CompactSublatt S)
let x, y be Element of S; ::_thesis: ( x in the carrier of (CompactSublatt S) & y in the carrier of (CompactSublatt S) & ex_inf_of {x,y},S implies inf {x,y} in the carrier of (CompactSublatt S) )
assume that
A4: x in the carrier of (CompactSublatt S) and
A5: y in the carrier of (CompactSublatt S) and
 ex_inf_of {x,y},S ; ::_thesis: inf {x,y} in the carrier of (CompactSublatt S)
A6: ( [y,(Bottom T)] `1 = y & [y,(Bottom T)] `2 = Bottom T ) ;
 y is compact by A5, WAYBEL_8:def_1;
then  [y,(Bottom T)] is compact by A3, A6, Th23, WAYBEL_3:15;
then A7: [y,(Bottom T)] in the carrier of (CompactSublatt [:S,T:]) by WAYBEL_8:def_1;
A8: ( [x,(Bottom T)] `1 = x & [x,(Bottom T)] `2 = Bottom T ) ;
 x is compact by A4, WAYBEL_8:def_1;
then  [x,(Bottom T)] is compact by A3, A8, Th23, WAYBEL_3:15;
then  ( ex_inf_of {[x,(Bottom T)],[y,(Bottom T)]},[:S,T:] & [x,(Bottom T)] in the carrier of (CompactSublatt [:S,T:]) ) by WAYBEL_8:def_1, YELLOW_0:21;
then  inf {[x,(Bottom T)],[y,(Bottom T)]} in the carrier of (CompactSublatt [:S,T:]) by A2, A7, YELLOW_0:def_16;
then A9: inf {[x,(Bottom T)],[y,(Bottom T)]} is compact by WAYBEL_8:def_1;
(inf {[x,(Bottom T)],[y,(Bottom T)]}) `1 = ([x,(Bottom T)] "/\" [y,(Bottom T)]) `1 by YELLOW_0:40
.= ([x,(Bottom T)] `1) "/\" ([y,(Bottom T)] `1) by Th13
.= x "/\" ([y,(Bottom T)] `1)
.= x "/\" y ;
then  x "/\" y is compact by A3, A9, Th22;
then  inf {x,y} is compact by YELLOW_0:40;
hence  inf {x,y} in the carrier of (CompactSublatt S) by WAYBEL_8:def_1; ::_thesis: verum
end;
thus  T is algebraic by A1, Th69; :: according to WAYBEL_8:def_5 ::_thesis: CompactSublatt T is meet-inheriting
let x, y be Element of T; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of (CompactSublatt T) or not y in the carrier of (CompactSublatt T) or not ex_inf_of {x,y},T or "/\" ({x,y},T) in the carrier of (CompactSublatt T) )
assume that
A10: x in the carrier of (CompactSublatt T) and
A11: y in the carrier of (CompactSublatt T) and
 ex_inf_of {x,y},T ; ::_thesis: "/\" ({x,y},T) in the carrier of (CompactSublatt T)
A12: ( [(Bottom S),y] `2 = y & [(Bottom S),y] `1 = Bottom S ) ;
 y is compact by A11, WAYBEL_8:def_1;
then  [(Bottom S),y] is compact by A3, A12, Th23, WAYBEL_3:15;
then A13: [(Bottom S),y] in the carrier of (CompactSublatt [:S,T:]) by WAYBEL_8:def_1;
A14: ( [(Bottom S),x] `2 = x & [(Bottom S),x] `1 = Bottom S ) ;
 x is compact by A10, WAYBEL_8:def_1;
then  [(Bottom S),x] is compact by A3, A14, Th23, WAYBEL_3:15;
then  ( ex_inf_of {[(Bottom S),x],[(Bottom S),y]},[:S,T:] & [(Bottom S),x] in the carrier of (CompactSublatt [:S,T:]) ) by WAYBEL_8:def_1, YELLOW_0:21;
then  inf {[(Bottom S),x],[(Bottom S),y]} in the carrier of (CompactSublatt [:S,T:]) by A2, A13, YELLOW_0:def_16;
then A15: inf {[(Bottom S),x],[(Bottom S),y]} is compact by WAYBEL_8:def_1;
(inf {[(Bottom S),x],[(Bottom S),y]}) `2 = ([(Bottom S),x] "/\" [(Bottom S),y]) `2 by YELLOW_0:40
.= ([(Bottom S),x] `2) "/\" ([(Bottom S),y] `2) by Th13
.= x "/\" ([(Bottom S),y] `2)
.= x "/\" y ;
then  x "/\" y is compact by A3, A15, Th22;
then  inf {x,y} is compact by YELLOW_0:40;
hence  "/\" ({x,y},T) in the carrier of (CompactSublatt T) by WAYBEL_8:def_1; ::_thesis: verum
end;