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 M3( the carrier of [:S,T:]) st
( b₁ in D & ( for b₂ being M3( 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 M3( the carrier of [:S,T:]) st
( b₁ in D & ( for b₂ being M3( the carrier of [:S,T:]) holds
( not b₂ in D or not b₁ <= b₂ or b₂ 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 object 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 object such that
A10: [t1,t] in D by A8, XTUPLE_0:def 13;
A11: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by YELLOW_3:def 2;
then reconsider s2 = 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 b<sub>1</sub> being M3( the carrier of [:S,T:]) holds
( not b<sub>1</sub> in D or not z <= b<sub>1</sub> or b<sub>1</sub> in [:X,Y:] ) ) )
thus z in D by A12; :: thesis: for b<sub>1</sub> being M3( the carrier of [:S,T:]) holds
( not b<sub>1</sub> in D or not z <= b<sub>1</sub> or b<sub>1</sub> 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