let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for X being Subset of st X is property(S) holds
( proj1 X is property(S) & proj2 X is property(S) )
let X be Subset of ; :: 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 st sup D in X holds
ex y being Element of st
( y in D & ( for x being Element of 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 ; :: thesis: ( sup D in proj1 X implies ex z being M2(the carrier of S) st
( z in D & ( for x being Element of 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 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 RELAT_1:def 4;
reconsider t = t as Element of by A2, A3, ZFMISC_1:106;
reconsider t' = {t} as non empty directed Subset of by WAYBEL_0:5;
ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75;
then sup [:D,t':] = [(sup (proj1 [:D,t':])),(sup (proj2 [:D,t':]))] by YELLOW_3:46
.= [(sup D),(sup (proj2 [:D,t':]))] by FUNCT_5:11
.= [(sup D),(sup t')] by FUNCT_5:11
.= [(sup D),t] by YELLOW_0:39 ;
then consider y being Element of such that
A4: y in [:D,t':] and
A5: for x being Element of st x in [:D,t':] & x >= y holds
x in X by A1, A3;
take z = y `1 ; :: thesis: ( z in D & ( for x being Element of st x in D & x >= z holds
x in proj1 X ) )
A6: y = [(y `1 ),(y `2 )] by A2, MCART_1:23;
hence z in D by A4, ZFMISC_1:106; :: thesis: for x being Element of st x in D & x >= z holds
x in proj1 X
A7: y `2 = t by A4, A6, ZFMISC_1:129;
let x be Element of ; :: 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,t':] by ZFMISC_1:129;
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 FUNCT_5:4; :: thesis: verum

end;

let D be non empty directed Subset of ; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" D,T in proj2 X or ex b₁ being M2(the carrier of T) st
( b₁ in D & ( for b₂ being M2(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 M2(the carrier of T) st
( b₁ in D & ( for b₂ being M2(the carrier of T) holds
( not b₂ in D or not b₁ <= b₂ or b₂ in proj2 X ) ) )
then consider s being set such that
A10: [s,(sup D)] in X by RELAT_1:def 5;
reconsider s = s as Element of by A2, A10, ZFMISC_1:106;
reconsider s' = {s} as non empty directed Subset of by WAYBEL_0:5;
ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75;
then sup [:s',D:] = [(sup (proj1 [:s',D:])),(sup (proj2 [:s',D:]))] by YELLOW_3:46
.= [(sup s'),(sup (proj2 [:s',D:]))] by FUNCT_5:11
.= [(sup s'),(sup D)] by FUNCT_5:11
.= [s,(sup D)] by YELLOW_0:39 ;
then consider y being Element of such that
A11: y in [:s',D:] and
A12: for x being Element of st x in [:s',D:] & x >= y holds
x in X by A1, A10;
take z = y `2 ; :: thesis: ( z in D & ( for b<sub>1</sub> being M2(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:23;
hence z in D by A11, ZFMISC_1:106; :: thesis: for b<sub>1</sub> being M2(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:128;
let x be Element of ; :: 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 [:s',D:] by ZFMISC_1:128;
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 FUNCT_5:4; :: thesis: verum