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, WAYBEL_1:def 8;
reconsider g = f " as Function of L2,L1 by A3, WAYBEL_0:67;
A5: g is isomorphic by A3, WAYBEL_0:68;
A7: L2 is up-complete by A1, A2, WAYBEL13:30;
A8: ( L1 is non empty up-complete Poset & L2 is non empty up-complete Poset ) by A1, A2, WAYBEL13:30;

now

let y be Element of L2; :: thesis: y = sup (waybelow y)
f is sups-preserving by A3, WAYBEL13:20;
then A9: f preserves_sup_of waybelow (g . y) by WAYBEL_0:def 33;
A10: ex_sup_of waybelow (g . y),L1 by A2, WAYBEL_0:75;
y in the carrier of L2 ;
then A11: y in rng f by A3, WAYBEL_0:66;
hence y = f . (g . y) by A3, FUNCT_1:57
.= f . (sup (waybelow (g . y))) by A2, WAYBEL_3:def 5
.= sup (f .: (waybelow (g . y))) by A9, A10, WAYBEL_0:def 31
.= sup (waybelow (f . (g . y))) by A3, A8, Th10
.= sup (waybelow y) by A3, A11, FUNCT_1:57 ;
:: thesis: verum

end;

then A12: L2 is satisfying_axiom_of_approximation by WAYBEL_3:def 5;

now

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 )

now

let u be set ; :: 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 set such that
v in dom g and
A13: v in Y and
A14: u = g . v by FUNCT_1:def 12;
v in waybelow y by A13;
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
A15: v1 = v and
A16: v1 << y ;
g . v1 << g . y by A5, A8, A16, WAYBEL13:27;
hence u in waybelow (g . y) by A14, A15, 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
A17: x in waybelow (g . y) and
A18: x is_>=_than X by A2, WAYBEL_0:1;
take z = f . x; :: thesis: ( z in waybelow y & z is_>=_than Y )
y in the carrier of L2 ;
then y in rng f by A3, WAYBEL_0:66;
then A19: f . (g . y) = y by A3, FUNCT_1:57;
x << g . y by A17, WAYBEL_3:7;
then z << y by A3, A8, A19, WAYBEL13:27;
hence z in waybelow y by WAYBEL_3:7; :: thesis: z is_>=_than Y
Y c= the carrier of L2 by XBOOLE_1:1;
then A20: Y c= rng f by A3, WAYBEL_0:66;
f .: X = f .: (f " Y) by A3, FUNCT_1:155
.= Y by A20, FUNCT_1:147 ;
hence z is_>=_than Y by A3, A18, WAYBEL13:19; :: thesis: verum

end;

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

end;

hence L2 is continuous by A7, A12, WAYBEL_3:def 6; :: thesis: verum