for S1, T1, S2, T2 being non empty RelStr st RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) & RelStr(# the carrier of T1, the InternalRel of T1 #) = RelStr(# the carrier of T2, the InternalRel of T2 #) holds
for f1 being Function of S1,T1
for f2 being Function of S2,T2 st f1 = f2 holds
( ( f1 is sups-preserving implies f2 is sups-preserving ) & ( f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving ) )