for S1, S2, T1, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of T1, the InternalRel of T1 #) & RelStr(# the carrier of S2, the InternalRel of S2 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f being Function of S1,S2
for g being Function of T1,T2 st f = g holds
for X being Subset of S1
for Y being Subset of T1 st X = Y holds
( ( f preserves_sup_of X implies g preserves_sup_of Y ) & ( f preserves_inf_of X implies g preserves_inf_of Y ) )