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;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
A4: g is isomorphic by A3, WAYBEL_0:68;

now :: thesis: for Y being non empty directed Subset of L2 holds ex_sup_of Y,L2

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

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

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

now :: thesis: for v being object st v in f .: X1 holds
v in Y

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

A12: now :: thesis: for y being Element of L2 st Y is_<=_than y holds
f . x <= y

let y be Element of L2; :: thesis: ( Y is_<=_than y implies f . x <= y )
assume Y is_<=_than y ; :: thesis: f . x <= y
then X is_<=_than g . y by A4, Th19;
then x <= g . y by A11;
then A13: f . x <= f . (g . y) by A3, WAYBEL_0:66;
y in the carrier of L2 ;
then y in dom g by FUNCT_2:def 1;
then y in rng f by A3, FUNCT_1:33;
hence f . x <= y by A3, A13, FUNCT_1:35; :: thesis: verum

end;

f .: X = f .: (f " Y) by A3, FUNCT_1:85
.= Y by A5, FUNCT_1:77 ;
then Y is_<=_than f . x by A3, A10, Th19;
hence ex_sup_of Y,L2 by A12, YELLOW_0:15; :: thesis: verum

end;

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