let L1 be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: according to WAYBEL11:def 2 :: thesis: Y is directly_closed
let E be non empty directed Subset of L2; :: according to WAYBEL11:def 2 :: thesis: ( not E c= Y or "\/" (E,L2) in Y )
assume A4: E c= Y ; :: thesis: "\/" (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; :: thesis: verum