let S, T be non empty reflexive antisymmetric up-complete RelStr ; 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; 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; ( 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
; WAYBEL11:def 2 [:X,Y:] is directly_closed
let D be non empty directed Subset of [:S,T:]; WAYBEL11:def 2 ( not D c= [:X,Y:] or "\/" (D,[:S,T:]) in [:X,Y:] )
assume A3:
D c= [:X,Y:]
; "\/" (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; verum