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,Y:] is closed_under_directed_sups holds
( ( Y <> {} implies X is closed_under_directed_sups ) & ( X <> {} implies Y is closed_under_directed_sups ) )
let X be Subset of S; :: thesis: for Y being Subset of T st [:X,Y:] is closed_under_directed_sups holds
( ( Y <> {} implies X is closed_under_directed_sups ) & ( X <> {} implies Y is closed_under_directed_sups ) )
let Y be Subset of T; :: thesis: ( [:X,Y:] is closed_under_directed_sups implies ( ( Y <> {} implies X is closed_under_directed_sups ) & ( X <> {} implies Y is closed_under_directed_sups ) ) )
assume A1: for D being non empty directed Subset of [:S,T:] st D c= [:X,Y:] holds
sup D in [:X,Y:] ; :: according to WAYBEL11:def 2 :: thesis: ( ( Y <> {} implies X is closed_under_directed_sups ) & ( X <> {} implies Y is closed_under_directed_sups ) )

hereby :: thesis: ( X <> {} implies Y is closed_under_directed_sups )

assume A2: Y <> {} ; :: thesis: X is closed_under_directed_sups
thus X is closed_under_directed_sups :: thesis: verum

proof

let D be non empty directed Subset of S; :: according to WAYBEL11:def 2 :: thesis: ( not D c= X or "\/" D,S in X )
assume A3: D c= X ; :: thesis: "\/" D,S in X
consider t being set such that
A4: t in Y by A2, XBOOLE_0:def 1;
reconsider t' = {t} as non empty directed Subset of T by A4, WAYBEL_0:5;
A5: t' c= Y by A4, ZFMISC_1:37;
ex_sup_of [:D,t':],[:S,T:] by WAYBEL_0:75;
then A6: sup [:D,t':] = [(sup (proj1 [:D,t':])),(sup (proj2 [:D,t':]))] by YELLOW_3:46
.= [(sup D),(sup (proj2 [:D,t':]))] by FUNCT_5:11
.= [(sup D),(sup t')] by FUNCT_5:11
.= [(sup D),t] by A4, YELLOW_0:39 ;
sup [:D,t':] in [:X,Y:] by A1, A3, A5, ZFMISC_1:119;
hence "\/" D,S in X by A6, ZFMISC_1:106; :: thesis: verum

end;

end;

assume A7: X <> {} ; :: thesis: Y is closed_under_directed_sups
let D be non empty directed Subset of T; :: according to WAYBEL11:def 2 :: thesis: ( not D c= Y or "\/" D,T in Y )
assume A8: D c= Y ; :: thesis: "\/" D,T in Y
consider s being set such that
A9: s in X by A7, XBOOLE_0:def 1;
reconsider s' = {s} as non empty directed Subset of S by A9, WAYBEL_0:5;
A10: s' c= X by A9, ZFMISC_1:37;
ex_sup_of [:s',D:],[:S,T:] by WAYBEL_0:75;
then A11: sup [:s',D:] = [(sup (proj1 [:s',D:])),(sup (proj2 [:s',D:]))] by YELLOW_3:46
.= [(sup s'),(sup (proj2 [:s',D:]))] by FUNCT_5:11
.= [(sup s'),(sup D)] by FUNCT_5:11
.= [s,(sup D)] by A9, YELLOW_0:39 ;
sup [:s',D:] in [:X,Y:] by A1, A8, A10, ZFMISC_1:119;
hence "\/" D,T in Y by A11, ZFMISC_1:106; :: thesis: verum