theorem :: YELLOW12:19

for L1 being 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 property(S) holds
Y is property(S)