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 M3( 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 M3( 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 object 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 b₁ being M3( the carrier of T) st
( b₁ in D & ( for b₂ being M3( the carrier of T) holds
( not b₂ in D or not b₁ <= b₂ or b₂ in proj2 X ) ) ) )
assume sup D in proj2 X ; :: thesis: ex b₁ being M3( the carrier of T) st
( b₁ in D & ( for b₂ being M3( the carrier of T) holds
( not b₂ in D or not b₁ <= b₂ or b₂ in proj2 X ) ) )
then consider s being object 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 b<sub>1</sub> being M3( the carrier of T) holds
( not b<sub>1</sub> in D or not z <= b<sub>1</sub> or b<sub>1</sub> 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 b<sub>1</sub> being M3( the carrier of T) holds
( not b<sub>1</sub> in D or not z <= b<sub>1</sub> or b<sub>1</sub> 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