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 ;
A4: ( L1 is non empty up-complete Poset & L2 is non empty up-complete Poset ) by ;
now :: thesis: for y being Element of L2 holds y = sup ()
let y be Element of L2; :: thesis: y = sup ()
A5: ex_sup_of waybelow (g . y),L1 by ;
f is sups-preserving by ;
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 ;
hence y = f . (g . y) by
.= f . (sup (waybelow (g . y))) by
.= sup (f .: (waybelow (g . y))) by
.= sup (waybelow (f . (g . y))) by A3, A4, Th8
.= sup () by ;
:: thesis: verum
end;
then A8: L2 is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
A9: g is isomorphic by ;
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 () ex z being Element of L2 st
( z in waybelow y & z is_>=_than Y )
proof
let Y be finite Subset of (); :: 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 ;
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 ;
hence u in waybelow (g . y) by ; :: 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 ;
y in the carrier of L2 ;
then y in rng f by ;
then A18: f . (g . y) = y by ;
take z = f . x; :: thesis: ( z in waybelow y & z is_>=_than Y )
x << g . y by ;
then z << y by ;
hence z in waybelow y by WAYBEL_3:7; :: thesis:
f .: X = f .: (f " Y) by
.= Y by ;
hence z is_>=_than Y by ; :: 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 ;
hence L2 is continuous by ; :: thesis: verum