let L1 be non empty reflexive antisymmetric up-complete RelStr ; for L2 being non empty reflexive RelStr
for X being Subset of L1
for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed holds
Y is directly_closed
let L2 be non empty reflexive RelStr ; for X being Subset of L1
for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed holds
Y is directly_closed
let X be Subset of L1; for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed holds
Y is directly_closed
let Y be Subset of L2; ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed implies Y is directly_closed )
assume that
A1:
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #)
and
A2:
X = Y
and
A3:
for D being non empty directed Subset of L1 st D c= X holds
sup D in X
; WAYBEL11:def 2 Y is directly_closed
let E be non empty directed Subset of L2; WAYBEL11:def 2 ( not E c= Y or "\/" (E,L2) in Y )
assume A4:
E c= Y
; "\/" (E,L2) in Y
reconsider D = E as non empty directed Subset of L1 by A1, WAYBEL_0:3;
( ex_sup_of D,L1 & sup D in X )
by A2, A3, A4, WAYBEL_0:75;
hence
"\/" (E,L2) in Y
by A1, A2, YELLOW_0:26; verum