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

now :: thesis: for y being Element of L2 holds y = sup (waybelow y)

let y be Element of L2; :: thesis: y = sup (waybelow y)
A5: ex_sup_of waybelow (g . y),L1 by A2, WAYBEL_0:75;
f is sups-preserving by A3, WAYBEL13:20;
then A6: f preserves_sup_of waybelow (g . y) by WAYBEL_0:def 33;
y in the carrier of L2 ;
then A7: y in rng f by A3, WAYBEL_0:66;
hence y = f . (g . y) by A3, FUNCT_1:35
.= f . (sup (waybelow (g . y))) by A2, WAYBEL_3:def 5
.= sup (f .: (waybelow (g . y))) by A6, A5, WAYBEL_0:def 31
.= sup (waybelow (f . (g . y))) by A3, A4, Th8
.= sup (waybelow y) by A3, A7, FUNCT_1:35 ;
:: thesis: verum

end;

then A8: L2 is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
A9: g is isomorphic by A3, WAYBEL_0:68;

A10: now :: thesis: for y being Element of L2 holds
( not waybelow y is empty & waybelow y is directed )

let y be Element of L2; :: thesis: ( not waybelow y is empty & waybelow y is directed )
for Y being finite Subset of (waybelow y) ex z being Element of L2 st
( z in waybelow y & z is_>=_than Y )

proof

let Y be finite Subset of (waybelow y); :: thesis: ex z being Element of L2 st
( z in waybelow y & z is_>=_than Y )
Y c= the carrier of L2 by XBOOLE_1:1;
then A11: Y c= rng f by A3, WAYBEL_0:66;

now :: thesis: for u being object st u in g .: Y holds
u in waybelow (g . y)

let u be object ; :: thesis: ( u in g .: Y implies u in waybelow (g . y) )
assume u in g .: Y ; :: thesis: u in waybelow (g . y)
then consider v being object such that
v in dom g and
A12: v in Y and
A13: u = g . v by FUNCT_1:def 6;
v in waybelow y by A12;
then v in { k where k is Element of L2 : k << y } by WAYBEL_3:def 3;
then consider v1 being Element of L2 such that
A14: v1 = v and
A15: v1 << y ;
g . v1 << g . y by A9, A4, A15, WAYBEL13:27;
hence u in waybelow (g . y) by A13, A14, WAYBEL_3:7; :: thesis: verum

end;

then reconsider X = g .: Y as finite Subset of (waybelow (g . y)) by TARSKI:def 3;
consider x being Element of L1 such that
A16: x in waybelow (g . y) and
A17: x is_>=_than X by A2, WAYBEL_0:1;
y in the carrier of L2 ;
then y in rng f by A3, WAYBEL_0:66;
then A18: f . (g . y) = y by A3, FUNCT_1:35;
take z = f . x; :: thesis: ( z in waybelow y & z is_>=_than Y )
x << g . y by A16, WAYBEL_3:7;
then z << y by A3, A4, A18, WAYBEL13:27;
hence z in waybelow y by WAYBEL_3:7; :: thesis: z is_>=_than Y
f .: X = f .: (f " Y) by A3, FUNCT_1:85
.= Y by A11, FUNCT_1:77 ;
hence z is_>=_than Y by A3, A17, WAYBEL13:19; :: thesis: verum

end;

hence ( not waybelow y is empty & waybelow y is directed ) by WAYBEL_0:1; :: thesis: verum

end;

L2 is up-complete by A1, A2, WAYBEL13:30;
hence L2 is continuous by A8, A10, WAYBEL_3:def 6; :: thesis: verum