let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for X being upper Subset of S
for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible
let X be upper Subset of S; :: thesis: for Y being upper Subset of T st X is inaccessible & Y is inaccessible holds
[:X,Y:] is inaccessible
let Y be upper Subset of T; :: thesis: ( X is inaccessible & Y is inaccessible implies [:X,Y:] is inaccessible )
assume that
A1: for D being non empty directed Subset of S st sup D in X holds
D meets X and
A2: for D being non empty directed Subset of T st sup D in Y holds
D meets Y ; :: according to WAYBEL11:def 1 :: thesis: [:X,Y:] is inaccessible
let D be non empty directed Subset of [:S,T:]; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" (D,[:S,T:]) in [:X,Y:] or not D misses [:X,Y:] )
assume A3: sup D in [:X,Y:] ; :: thesis: not D misses [: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 proj1 D meets X by A1;
then consider s being object such that
A5: s in proj1 D and
A6: s in X by XBOOLE_0:3;
reconsider s = s as Element of S by A5;
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 proj2 D meets Y by A2;
then consider t being object such that
A8: t in proj2 D and
A9: t in Y by XBOOLE_0:3;
reconsider t = t as Element of T by A8;
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;

now :: thesis: ex z being Element of [:S,T:] st
( z in D & z in [:X,Y:] )

take z = z; :: thesis: ( z in D & z in [:X,Y:] )
thus z in D by A12; :: thesis: z in [:X,Y:]
A15: z = [(z `1),(z `2)] by A11, MCART_1:21;
then t <= z `2 by A14, YELLOW_3:11;
then A16: z `2 in Y by A9, WAYBEL_0:def 20;
s <= z `1 by A13, A15, YELLOW_3:11;
then z `1 in X by A6, WAYBEL_0:def 20;
hence z in [:X,Y:] by A15, A16, ZFMISC_1:87; :: thesis: verum

end;

hence not D misses [:X,Y:] by XBOOLE_0:3; :: thesis: verum