let L1, L2 be sup-Semilattice; :: thesis: ( L1,L2 are_isomorphic & L1 is lower-bounded & L1 is algebraic implies L2 is algebraic )
assume that
A1: L1,L2 are_isomorphic and
A2: ( L1 is lower-bounded & L1 is algebraic ) ; :: thesis: L2 is algebraic
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;

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

let y be Element of L2; :: thesis: ( not compactbelow y is empty & compactbelow y is directed )
y in the carrier of L2 ;
then y in dom g by FUNCT_2:def 1;
then A6: y in rng f by A3, FUNCT_1:33;
A7: L2 is non empty up-complete Poset by A1, A2, Th30;
A8: ( not compactbelow (g . y) is empty & compactbelow (g . y) is directed ) by A2, WAYBEL_8:def 4;

now :: thesis: for Y being finite Subset of (compactbelow (f . (g . y))) ex fx being Element of the carrier of L2 st
( fx in compactbelow (f . (g . y)) & fx is_>=_than Y )

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

now :: thesis: for z being object st z in g .: Y holds
z in compactbelow (g . y)

let z be object ; :: thesis: ( z in g .: Y implies z in compactbelow (g . y) )
assume z in g .: Y ; :: thesis: z in compactbelow (g . y)
then consider v being object such that
A10: v in dom g and
A11: v in Y and
A12: z = g . v by FUNCT_1:def 6;
reconsider v = v as Element of L2 by A10;
v in compactbelow (f . (g . y)) by A11;
then v in compactbelow y by A3, A6, FUNCT_1:35;
then v <= y by WAYBEL_8:4;
then A13: g . v <= g . y by A4, WAYBEL_0:66;
v is compact by A11, WAYBEL_8:4;
then g . v is compact by A2, A4, A7, Th28;
hence z in compactbelow (g . y) by A12, A13, WAYBEL_8:4; :: thesis: verum

end;

then reconsider X = g .: Y as finite Subset of (compactbelow (g . y)) by TARSKI:def 3;
consider x being Element of L1 such that
A14: x in compactbelow (g . y) and
A15: x is_>=_than X by A8, WAYBEL_0:1;
take fx = f . x; :: thesis: ( fx in compactbelow (f . (g . y)) & fx is_>=_than Y )
x <= g . y by A14, WAYBEL_8:4;
then A16: f . x <= f . (g . y) by A3, WAYBEL_0:66;
x is compact by A14, WAYBEL_8:4;
then f . x is compact by A2, A3, A7, Th28;
hence fx in compactbelow (f . (g . y)) by A16, WAYBEL_8:4; :: thesis: fx is_>=_than Y
f .: X = f .: (f " Y) by A3, FUNCT_1:85
.= Y by A9, FUNCT_1:77 ;
hence fx is_>=_than Y by A3, A15, Th19; :: thesis: verum

end;

then ( not compactbelow (f . (g . y)) is empty & compactbelow (f . (g . y)) is directed ) by WAYBEL_0:1;
hence ( not compactbelow y is empty & compactbelow y is directed ) by A3, A6, FUNCT_1:35; :: thesis: verum

end;

( L2 is up-complete & L2 is satisfying_axiom_K ) by A1, A2, Th30, Th31;
hence L2 is algebraic by A5, WAYBEL_8:def 4; :: thesis: verum