let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for X being Subset of [:S,T:] st X is inaccessible_by_directed_joins holds
( proj1 X is inaccessible_by_directed_joins & proj2 X is inaccessible_by_directed_joins )
let X be Subset of [:S,T:]; :: thesis: ( X is inaccessible_by_directed_joins implies ( proj1 X is inaccessible_by_directed_joins & proj2 X is inaccessible_by_directed_joins ) )
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_by_directed_joins & proj2 X is inaccessible_by_directed_joins )
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_by_directed_joins

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 RELAT_1:def 4;
A4: t in the carrier of T by A2, A3, ZFMISC_1:106;
then reconsider t' = {t} as non empty directed Subset of T 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 A4, YELLOW_0:39 ;
then [:D,{t}:] meets X by A1, A3;
then consider x being set such that
A5: ( x in [:D,{t}:] & x in X ) by XBOOLE_0:3;
thus D meets proj1 X :: thesis: verum

proof

now

take a = x `1 ; :: thesis: ( a in D & a in proj1 X )
x = [a,(x `2 )] by A5, MCART_1:23;
hence ( a in D & a in proj1 X ) by A5, FUNCT_5:4, ZFMISC_1:106; :: thesis: verum

end;

hence D meets proj1 X by XBOOLE_0:3; :: thesis: verum

end;

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
A6: [s,(sup D)] in X by RELAT_1:def 5;
A7: s in the carrier of S by A2, A6, ZFMISC_1:106;
then reconsider s' = {s} as non empty directed Subset of S 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 A7, YELLOW_0:39 ;
then [:{s},D:] meets X by A1, A6;
then consider x being set such that
A8: ( x in [:{s},D:] & x in X ) by XBOOLE_0:3;

now

take a = x `2 ; :: thesis: ( a in D & a in proj2 X )
x = [(x `1 ),a] by A8, MCART_1:23;
hence ( a in D & a in proj2 X ) by A8, FUNCT_5:4, ZFMISC_1:106; :: thesis: verum

end;

hence not D misses proj2 X by XBOOLE_0:3; :: thesis: verum