theorem Th8: :: WAYBEL15:8

for L1, L2 being non empty up-complete Poset
for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds f .: (waybelow x) = waybelow (f . x)