for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x, y being Element of L1 holds
( x << y iff f . x << f . y )