let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for X being Subset of [:S,T:] st X is inaccessible holds
( proj1 X is inaccessible & proj2 X is inaccessible )
let X be Subset of [:S,T:]; :: thesis: ( X is inaccessible implies ( proj1 X is inaccessible & proj2 X is inaccessible ) )
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 & proj2 X is inaccessible )
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
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 object such that
A3: [(sup D),t] in X by XTUPLE_0:def 12;
A4: t in the carrier of T by A2, A3, ZFMISC_1:87;
then 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 A4, YELLOW_0:39 ;
then [:D,{t}:] meets X by A1, A3;
then consider x being object such that
A5: x in [:D,{t}:] and
A6: x in X by XBOOLE_0:3;
now :: thesis: ex a being object st
( a in D & a in proj1 X )
take a = x `1 ; :: thesis: ( a in D & a in proj1 X )
x = [a,(x `2)] by A5, MCART_1:21;
hence ( a in D & a in proj1 X ) by A5, A6, XTUPLE_0:def 12, ZFMISC_1:87; :: thesis: verum
end;
hence D meets proj1 X by XBOOLE_0:3; :: thesis: verum
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 object such that
A7: [s,(sup D)] in X by XTUPLE_0:def 13;
A8: s in the carrier of S by A2, A7, ZFMISC_1:87;
then 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 A8, YELLOW_0:39 ;
then [:{s},D:] meets X by A1, A7;
then consider x being object such that
A9: x in [:{s},D:] and
A10: x in X by XBOOLE_0:3;
now :: thesis: ex a being object st
( a in D & a in proj2 X )
take a = x `2 ; :: thesis: ( a in D & a in proj2 X )
x = [(x `1),a] by A9, MCART_1:21;
hence ( a in D & a in proj2 X ) by A9, A10, XTUPLE_0:def 13, ZFMISC_1:87; :: thesis: verum
end;
hence not D misses proj2 X by XBOOLE_0:3; :: thesis: verum