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 closed_under_directed_sups holds
Y is closed_under_directed_sups
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 closed_under_directed_sups holds
Y is closed_under_directed_sups
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 closed_under_directed_sups holds
Y is closed_under_directed_sups
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 closed_under_directed_sups implies Y is closed_under_directed_sups )
assume that
A1: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & X = Y ) and
A2: 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 closed_under_directed_sups
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 A3: E c= Y ; :: thesis: "\/" E,L2 in Y
reconsider D = E as non empty directed Subset of L1 by A1, WAYBEL_0:3;
A4: ex_sup_of D,L1 by WAYBEL_0:75;
sup D in X by A1, A2, A3;
hence "\/" E,L2 in Y by A1, A4, YELLOW_0:26; :: thesis: verum