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 b₁ being M2(the carrier of [:S,T:]) st
( b₁ in D & ( for b₂ being M2(the carrier of [:S,T:]) holds
( not b₂ in D or not b₁ <= b₂ or b₂ in [:X,Y:] ) ) ) )
assume A3: sup D in [:X,Y:] ; :: thesis: ex b₁ being M2(the carrier of [:S,T:]) st
( b₁ in D & ( for b₂ being M2(the carrier of [:S,T:]) holds
( not b₂ in D or not b₁ <= b₂ or b₂ in [:X,Y:] ) ) )
A4: ( not proj1 D is empty & proj1 D is directed & not proj2 D is empty & proj2 D is directed ) by YELLOW_3:21, YELLOW_3:22;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
then A5: ( sup (proj1 D) in X & sup (proj2 D) in Y ) by A3, ZFMISC_1:106;
then consider s being Element of S such that
A6: s in proj1 D and
A7: for x being Element of S st x in proj1 D & x >= s holds
x in X by A1, A4;
consider t being Element of T such that
A8: t in proj2 D and
A9: for x being Element of T st x in proj2 D & x >= t holds
x in Y by A2, A4, A5;
consider s2 being set such that
A10: [s,s2] in D by A6, RELAT_1:def 4;
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 A10, ZFMISC_1:106;
consider t1 being set such that
A12: [t1,t] in D by A8, RELAT_1:def 5;
reconsider t1 = t1 as Element of S by A11, A12, ZFMISC_1:106;
consider z being Element of [:S,T:] such that
A13: z in D and
A14: ( [s,s2] <= z & [t1,t] <= z ) by A10, A12, WAYBEL_0:def 1;
take z ; :: thesis: ( z in D & ( for b₁ being M2(the carrier of [:S,T:]) holds
( not b₁ in D or not z <= b₁ or b₁ in [:X,Y:] ) ) )
thus z in D by A13; :: thesis: for b₁ being M2(the carrier of [:S,T:]) holds
( not b₁ in D or not z <= b₁ or b₁ 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 A15: x in D ; :: thesis: ( not z <= x or x in [:X,Y:] )
assume x >= z ; :: thesis: x in [:X,Y:]
then A16: ( x `1 >= z `1 & x `2 >= z `2 ) by YELLOW_3:12;
A17: x = [(x `1 ),(x `2 )] by A11, MCART_1:23;
then A18: ( x `1 in proj1 D & x `2 in proj2 D ) by A15, FUNCT_5:4;
z = [(z `1 ),(z `2 )] by A11, MCART_1:23;
then ( s <= z `1 & t <= z `2 ) by A14, YELLOW_3:11;
then ( x `1 >= s & x `2 >= t ) by A16, ORDERS_2:26;
then ( x `1 in X & x `2 in Y ) by A7, A9, A18;
hence x in [:X,Y:] by A17, ZFMISC_1:106; :: thesis: verum