let L1, L2 be non empty up-complete Poset; :: thesis: 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 )
let f be Function of L1,L2; :: thesis: ( f is isomorphic implies for x, y being Element of L1 holds
( x << y iff f . x << f . y ) )
assume A1: f is isomorphic ; :: thesis: for x, y being Element of L1 holds
( x << y iff f . x << f . y )
then A2: f is one-to-one ;
reconsider g = f " as Function of L2,L1 by A1, WAYBEL_0:67;
let x, y be Element of L1; :: thesis: ( x << y iff f . x << f . y )
thus ( x << y implies f . x << f . y ) by A1, Lm5; :: thesis: ( f . x << f . y implies x << y )
thus ( f . x << f . y implies x << y ) :: thesis: verum

proof

( x in the carrier of L1 & y in the carrier of L1 & not the carrier of L2 is empty ) ;
then A3: ( x in dom f & y in dom f ) by FUNCT_2:def 1;
assume f . x << f . y ; :: thesis: x << y
then g . (f . x) << g . (f . y) by A1, Lm5, WAYBEL_0:68;
then x << g . (f . y) by A2, A3, FUNCT_1:56;
hence x << y by A2, A3, FUNCT_1:56; :: thesis: verum

end;