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 directly_closed holds
( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )
let X be Subset of S; :: thesis: for Y being Subset of T st [:X,Y:] is directly_closed holds
( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) )
let Y be Subset of T; :: thesis: ( [:X,Y:] is directly_closed implies ( ( Y <> {} implies X is directly_closed ) & ( X <> {} implies Y is directly_closed ) ) )
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 directly_closed ) & ( X <> {} implies Y is directly_closed ) )
hereby :: thesis: ( X <> {} implies Y is directly_closed )
assume A2: Y <> {} ; :: thesis: X is directly_closed
thus X is directly_closed :: thesis: verum
proof
consider t being object such that
A3: t in Y by A2, XBOOLE_0:def 1;
reconsider t9 = {t} as non empty directed Subset of T by A3, WAYBEL_0:5;
A4: t9 c= Y by A3, ZFMISC_1:31;
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 D c= X ; :: thesis: "\/" (D,S) in X
then A5: sup [:D,t9:] in [:X,Y:] by A1, A4, ZFMISC_1:96;
ex_sup_of [:D,t9:],[:S,T:] by WAYBEL_0:75;
then sup [:D,t9:] = [(sup (proj1 [:D,t9:])),(sup (proj2 [:D,t9:]))] by YELLOW_3:46
.= [(sup D),(sup (proj2 [:D,t9:]))] by FUNCT_5:9
.= [(sup D),(sup t9)] by FUNCT_5:9
.= [(sup D),t] by A3, YELLOW_0:39 ;
hence "\/" (D,S) in X by A5, ZFMISC_1:87; :: thesis: verum
end;
end;
assume X <> {} ; :: thesis: Y is directly_closed
then consider s being object such that
A6: s in X by XBOOLE_0:def 1;
reconsider s9 = {s} as non empty directed Subset of S by A6, WAYBEL_0:5;
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 A7: D c= Y ; :: thesis: "\/" (D,T) in Y
ex_sup_of [:s9,D:],[:S,T:] by WAYBEL_0:75;
then A8: sup [:s9,D:] = [(sup (proj1 [:s9,D:])),(sup (proj2 [:s9,D:]))] by YELLOW_3:46
.= [(sup s9),(sup (proj2 [:s9,D:]))] by FUNCT_5:9
.= [(sup s9),(sup D)] by FUNCT_5:9
.= [s,(sup D)] by A6, YELLOW_0:39 ;
s9 c= X by A6, ZFMISC_1:31;
then sup [:s9,D:] in [:X,Y:] by A1, A7, ZFMISC_1:96;
hence "\/" (D,T) in Y by A8, ZFMISC_1:87; :: thesis: verum