theorem Th28: :: WAYBEL13:28

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
( x is compact iff f . x is compact )