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 reconsider g = f " as Function of L2,L1 by 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, Lm4; :: thesis: ( f . x << f . y implies x << y )
thus ( f . x << f . y implies x << y ) :: thesis: verum
proof
y in the carrier of L1 ;
then A2: y in dom f by FUNCT_2:def 1;
x in the carrier of L1 ;
then A3: x 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, Lm4, WAYBEL_0:68;
then x << g . (f . y) by A1, A3, FUNCT_1:34;
hence x << y by A1, A2, FUNCT_1:34; :: thesis: verum
end;