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 st x << y holds
f . x << f . y
let f be Function of L1,L2; :: thesis: ( f is isomorphic implies for x, y being Element of L1 st x << y holds
f . x << f . y )
assume A1: f is isomorphic ; :: thesis: for x, y being Element of L1 st x << y holds
f . x << f . y
then A2: f is one-to-one ;
reconsider g = f " as Function of L2,L1 by A1, WAYBEL_0:67;
A3: g is isomorphic by A1, WAYBEL_0:68;
let x, y be Element of L1; :: thesis: ( x << y implies f . x << f . y )
assume A4: x << y ; :: thesis: f . x << f . y

now

let X be non empty directed Subset of L2; :: thesis: ( f . y <= sup X implies ex fc being Element of the carrier of L2 st
( fc in X & f . x <= fc ) )
X c= the carrier of L2 ;
then A5: X c= rng f by A1, WAYBEL_0:66;

now

let Y1 be finite Subset of (g .: X); :: thesis: ex gy1 being Element of the carrier of L1 st
( gy1 in g .: X & gy1 is_>=_than Y1 )

now

let v be set ; :: thesis: ( v in f .: Y1 implies v in X )
assume v in f .: Y1 ; :: thesis: v in X
then consider u being set such that
A6: u in dom f and
A7: u in Y1 and
A8: v = f . u by FUNCT_1:def 12;
v in f .: (g .: X) by A6, A7, A8, FUNCT_1:def 12;
then v in f .: (f " X) by A2, FUNCT_1:155;
hence v in X by A5, FUNCT_1:147; :: thesis: verum

end;

then reconsider X1 = f .: Y1 as finite Subset of X by TARSKI:def 3;
consider y1 being Element of L2 such that
A9: y1 in X and
A10: y1 is_>=_than X1 by WAYBEL_0:1;
take gy1 = g . y1; :: thesis: ( gy1 in g .: X & gy1 is_>=_than Y1 )
( not the carrier of L1 is empty & y1 in the carrier of L2 ) ;
then y1 in dom g by FUNCT_2:def 1;
hence gy1 in g .: X by A9, FUNCT_1:def 12; :: thesis: gy1 is_>=_than Y1
( Y1 c= the carrier of L1 & not the carrier of L2 is empty ) by XBOOLE_1:1;
then Y1 c= dom f by FUNCT_2:def 1;
then A11: Y1 c= f " (f .: Y1) by FUNCT_1:146;
A12: f " (f .: Y1) c= Y1 by A2, FUNCT_1:152;
g .: X1 = f " (f .: Y1) by A2, FUNCT_1:155
.= Y1 by A11, A12, XBOOLE_0:def 10 ;
hence gy1 is_>=_than Y1 by A3, A10, Th19; :: thesis: verum

end;

then reconsider Y = g .: X as non empty directed Subset of L1 by WAYBEL_0:1;
( y in the carrier of L1 & not the carrier of L2 is empty ) ;
then A13: y in dom f by FUNCT_2:def 1;
A14: ex_sup_of X,L2 by WAYBEL_0:75;
g is sups-preserving by A3;
then A15: g preserves_sup_of X by WAYBEL_0:def 33;
assume f . y <= sup X ; :: thesis: ex fc being Element of the carrier of L2 st
( fc in X & f . x <= fc )
then g . (f . y) <= g . (sup X) by A3, WAYBEL_0:66;
then y <= g . (sup X) by A2, A13, FUNCT_1:56;
then y <= sup Y by A14, A15, WAYBEL_0:def 31;
then consider c being Element of L1 such that
A16: c in Y and
A17: x <= c by A4, WAYBEL_3:def 1;
take fc = f . c; :: thesis: ( fc in X & f . x <= fc )
( c in the carrier of L1 & not the carrier of L2 is empty ) ;
then c in dom f by FUNCT_2:def 1;
then f . c in f .: Y by A16, FUNCT_1:def 12;
then f . c in f .: (f " X) by A2, FUNCT_1:155;
hence fc in X by A5, FUNCT_1:147; :: thesis: f . x <= fc
thus f . x <= fc by A1, A17, WAYBEL_0:66; :: thesis: verum

end;

hence f . x << f . y by WAYBEL_3:def 1; :: thesis: verum