let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for X being Subset of S
for Y being Subset of T st X is closed_under_directed_sups & Y is closed_under_directed_sups holds
[:X,Y:] is closed_under_directed_sups
let X be Subset of S; :: thesis: for Y being Subset of T st X is closed_under_directed_sups & Y is closed_under_directed_sups holds
[:X,Y:] is closed_under_directed_sups
let Y be Subset of T; :: thesis: ( X is closed_under_directed_sups & Y is closed_under_directed_sups implies [:X,Y:] is closed_under_directed_sups )
assume that
A1: for D being non empty directed Subset of S st D c= X holds
sup D in X and
A2: for D being non empty directed Subset of T st D c= Y holds
sup D in Y ; :: according to WAYBEL11:def 2 :: thesis: [:X,Y:] is closed_under_directed_sups
let D be non empty directed Subset of [:S,T:]; :: according to WAYBEL11:def 2 :: thesis: ( not D c= [:X,Y:] or "\/" D,[:S,T:] in [:X,Y:] )
assume D c= [:X,Y:] ; :: thesis: "\/" D,[:S,T:] in [:X,Y:]
then A3: ( proj1 D c= X & proj2 D c= Y ) by FUNCT_5:13;
( 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;
then A4: ( sup (proj1 D) in X & sup (proj2 D) in Y ) by A1, A2, A3;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
hence "\/" D,[:S,T:] in [:X,Y:] by A4, ZFMISC_1:106; :: thesis: verum