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;

A9: g is isomorphic by A3, WAYBEL_0:68;

hence L2 is continuous by A8, A10, WAYBEL_3:def 6; :: thesis: verum

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)

then A8:
L2 is satisfying_axiom_of_approximation
by WAYBEL_3:def 5;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;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

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 )

L2 is up-complete
by A1, A2, WAYBEL13:30;( 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 )

end;for Y being finite Subset of (waybelow y) ex z being Element of L2 st

( z in waybelow y & z is_>=_than Y )

proof

hence
( not waybelow y is empty & waybelow y is directed )
by WAYBEL_0:1; :: thesis: verum
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;

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;( 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)

then reconsider X = g .: Y as finite Subset of (waybelow (g . y)) by TARSKI:def 3;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;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

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

hence L2 is continuous by A8, A10, WAYBEL_3:def 6; :: thesis: verum