theorem Th66: :: WAYBEL_0:66

for S, T being non empty RelStr
for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )