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