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 property(S) holds
Y is property(S)
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 property(S) holds
Y is property(S)
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 property(S) holds
Y is property(S)
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 property(S) implies Y is property(S) )
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 sup D in X holds
ex y being Element of L1 st
( y in D & ( for x being Element of L1 st x in D & x >= y holds
x in X ) ) ; :: according to WAYBEL11:def 3 :: thesis: Y is property(S)
let E be non empty directed Subset of L2; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (E,L2) in Y or ex b₁ being Element of the carrier of L2 st
( b₁ in E & ( for b₂ being Element of the carrier of L2 holds
( not b₂ in E or not b₁ <= b₂ or b₂ in Y ) ) ) )
assume A4: sup E in Y ; :: thesis: ex b₁ being Element of the carrier of L2 st
( b₁ in E & ( for b₂ being Element of the carrier of L2 holds
( not b₂ in E or not b₁ <= b₂ or b₂ in Y ) ) )
reconsider D = E as non empty directed Subset of L1 by A1, WAYBEL_0:3;
ex_sup_of D,L1 by WAYBEL_0:75;
then sup D in X by A1, A2, A4, YELLOW_0:26;
then consider y being Element of L1 such that
A5: y in D and
A6: for x being Element of L1 st x in D & x >= y holds
x in X by A3;
reconsider y2 = y as Element of L2 by A1;
take y2 ; :: thesis: ( y2 in E & ( for b₁ being Element of the carrier of L2 holds
( not b₁ in E or not y2 <= b₁ or b₁ in Y ) ) )
thus y2 in E by A5; :: thesis: for b₁ being Element of the carrier of L2 holds
( not b₁ in E or not y2 <= b₁ or b₁ in Y )
let x2 be Element of L2; :: thesis: ( not x2 in E or not y2 <= x2 or x2 in Y )
assume ( x2 in E & x2 >= y2 ) ; :: thesis: x2 in Y
hence x2 in Y by A1, A2, A6, YELLOW_0:1; :: thesis: verum