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

now :: thesis: for X being non empty directed Subset of L2 st f . y <= sup X holds
ex fc being Element of the carrier of L2 st
( fc in X & f . x <= fc )

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 ) )
y in the carrier of L1 ;
then A4: y in dom f by FUNCT_2:def 1;
X c= the carrier of L2 ;
then A5: X c= rng f by A1, WAYBEL_0:66;

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

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 )
A6: f " (f .: Y1) c= Y1 by A1, FUNCT_1:82;

now :: thesis: for v being object st v in f .: Y1 holds
v in X

let v be object ; :: thesis: ( v in f .: Y1 implies v in X )
assume v in f .: Y1 ; :: thesis: v in X
then ex u being object st
( u in dom f & u in Y1 & v = f . u ) by FUNCT_1:def 6;
then v in f .: (g .: X) by FUNCT_1:def 6;
then v in f .: (f " X) by A1, FUNCT_1:85;
hence v in X by A5, FUNCT_1:77; :: 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
A7: y1 in X and
A8: y1 is_>=_than X1 by WAYBEL_0:1;
take gy1 = g . y1; :: thesis: ( gy1 in g .: X & gy1 is_>=_than Y1 )
y1 in the carrier of L2 ;
then y1 in dom g by FUNCT_2:def 1;
hence gy1 in g .: X by A7, FUNCT_1:def 6; :: thesis: gy1 is_>=_than Y1
Y1 c= the carrier of L1 by XBOOLE_1:1;
then Y1 c= dom f by FUNCT_2:def 1;
then A9: Y1 c= f " (f .: Y1) by FUNCT_1:76;
g .: X1 = f " (f .: Y1) by A1, FUNCT_1:85
.= Y1 by A9, A6, XBOOLE_0:def 10 ;
hence gy1 is_>=_than Y1 by A2, A8, Th19; :: thesis: verum

end;

then reconsider Y = g .: X as non empty directed Subset of L1 by WAYBEL_0:1;
A10: ( ex_sup_of X,L2 & g preserves_sup_of X ) by A2, WAYBEL_0:75, 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 A2, WAYBEL_0:66;
then y <= g . (sup X) by A1, A4, FUNCT_1:34;
then y <= sup Y by A10, WAYBEL_0:def 31;
then consider c being Element of L1 such that
A11: c in Y and
A12: x <= c by A3, WAYBEL_3:def 1;
take fc = f . c; :: thesis: ( fc in X & f . x <= fc )
c in the carrier of L1 ;
then c in dom f by FUNCT_2:def 1;
then f . c in f .: Y by A11, FUNCT_1:def 6;
then f . c in f .: (f " X) by A1, FUNCT_1:85;
hence fc in X by A5, FUNCT_1:77; :: thesis: f . x <= fc
thus f . x <= fc by A1, A12, WAYBEL_0:66; :: thesis: verum

end;

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