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_by_directed_joins & Y is inaccessible_by_directed_joins holds
[:X,Y:] is inaccessible_by_directed_joins
let X be upper Subset of S; :: thesis: for Y being upper Subset of T st X is inaccessible_by_directed_joins & Y is inaccessible_by_directed_joins holds
[:X,Y:] is inaccessible_by_directed_joins
let Y be upper Subset of T; :: thesis: ( X is inaccessible_by_directed_joins & Y is inaccessible_by_directed_joins implies [:X,Y:] is inaccessible_by_directed_joins )
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_by_directed_joins
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:]
A4: ( not proj1 D is empty & proj1 D is directed & not proj2 D is empty & proj2 D is directed ) by YELLOW_3:21, YELLOW_3:22;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
then ( sup (proj1 D) in X & sup (proj2 D) in Y ) by A3, ZFMISC_1:106;
then A5: ( proj1 D meets X & proj2 D meets Y ) by A1, A2, A4;
then consider s being set such that
A6: ( s in proj1 D & s in X ) by XBOOLE_0:3;
consider t being set such that
A7: ( t in proj2 D & t in Y ) by A5, XBOOLE_0:3;
reconsider s = s as Element of S by A6;
reconsider t = t as Element of T by A7;
consider s2 being set such that
A8: [s,s2] in D by A6, RELAT_1:def 4;
A9: 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 A8, ZFMISC_1:106;
consider t1 being set such that
A10: [t1,t] in D by A7, RELAT_1:def 5;
reconsider t1 = t1 as Element of S by A9, A10, ZFMISC_1:106;
consider z being Element of [:S,T:] such that
A11: z in D and
A12: ( [s,s2] <= z & [t1,t] <= z ) by A8, A10, WAYBEL_0:def 1;

now

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

end;

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