let L1, L2 be non empty Poset; :: thesis: ( L1,L2 are_isomorphic & L1 is up-complete implies L2 is up-complete )
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is up-complete ; :: thesis: L2 is up-complete
consider f being Function of L1,L2 such that
A3: f is isomorphic by A1, WAYBEL_1:def 8;
A4: f is one-to-one by A3;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
A5: g is isomorphic by A3, WAYBEL_0:68;

now

let Y be non empty directed Subset of L2; :: thesis: ex_sup_of Y,L2
Y c= the carrier of L2 ;
then A6: Y c= rng f by A3, WAYBEL_0:66;

now

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

now

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

end;

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

end;

then reconsider X = g .: Y as non empty directed Subset of L1 by WAYBEL_0:1;
ex_sup_of X,L1 by A2, WAYBEL_0:75;
then consider x being Element of L1 such that
A14: X is_<=_than x and
A15: for b being Element of L1 st X is_<=_than b holds
x <= b by YELLOW_0:15;
f .: X = f .: (f " Y) by A4, FUNCT_1:155
.= Y by A6, FUNCT_1:147 ;
then A16: Y is_<=_than f . x by A3, A14, Th19;

now

let y be Element of L2; :: thesis: ( Y is_<=_than y implies f . x <= y )
( not the carrier of L1 is empty & y in the carrier of L2 ) ;
then y in dom g by FUNCT_2:def 1;
then A17: y in rng f by A4, FUNCT_1:55;
assume Y is_<=_than y ; :: thesis: f . x <= y
then X is_<=_than g . y by A5, Th19;
then x <= g . y by A15;
then f . x <= f . (g . y) by A3, WAYBEL_0:66;
hence f . x <= y by A4, A17, FUNCT_1:57; :: thesis: verum

end;

hence ex_sup_of Y,L2 by A16, YELLOW_0:15; :: thesis: verum

end;

hence L2 is up-complete by WAYBEL_0:75; :: thesis: verum