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 directly_closed & Y is directly_closed holds
[:X,Y:] is directly_closed
let X be Subset of S; :: thesis: for Y being Subset of T st X is directly_closed & Y is directly_closed holds
[:X,Y:] is directly_closed
let Y be Subset of T; :: thesis: ( X is directly_closed & Y is directly_closed implies [:X,Y:] is directly_closed )
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 directly_closed
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 A3: D c= [:X,Y:] ; :: thesis: "\/" (D,[:S,T:]) in [:X,Y:]
( not proj2 D is empty & proj2 D is directed ) by YELLOW_3:21, YELLOW_3:22;
then A4: sup (proj2 D) in Y by A2, A3, FUNCT_5:11;
ex_sup_of D,[:S,T:] by WAYBEL_0:75;
then A5: sup D = [(sup (proj1 D)),(sup (proj2 D))] by YELLOW_3:46;
( not proj1 D is empty & proj1 D is directed ) by YELLOW_3:21, YELLOW_3:22;
then sup (proj1 D) in X by A1, A3, FUNCT_5:11;
hence "\/" (D,[:S,T:]) in [:X,Y:] by A4, A5, ZFMISC_1:87; :: thesis: verum