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
A3: ( ( for x being Element of L1 holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L1 is up-complete & L1 is satisfying_axiom_K ) by A2, WAYBEL_8:def 4;
consider f being Function of L1,L2 such that
A4: f is isomorphic by A1, WAYBEL_1:def 8;
reconsider g = f " as Function of L2,L1 by A4, WAYBEL_0:67;
A5: g is isomorphic by A4, WAYBEL_0:68;

A6: now

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

now

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 )

now

let z be set ; :: 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 set such that
A12: v in dom g and
A13: v in Y and
A14: z = g . v by FUNCT_1:def 12;
reconsider v = v as Element of L2 by A12;
v in compactbelow (f . (g . y)) by A13;
then v in compactbelow y by A7, A8, FUNCT_1:57;
then A15: ( v <= y & v is compact ) by WAYBEL_8:4;
then A16: g . v is compact by A5, A10, A11, Th28;
g . v <= g . y by A5, A15, WAYBEL_0:66;
hence z in compactbelow (g . y) by A14, A16, 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
A17: x in compactbelow (g . y) and
A18: x is_>=_than X by A9, WAYBEL_0:1;
take fx = f . x; :: thesis: ( fx in compactbelow (f . (g . y)) & fx is_>=_than Y )
A19: ( x <= g . y & x is compact ) by A17, WAYBEL_8:4;
then A20: f . x is compact by A4, A10, A11, Th28;
f . x <= f . (g . y) by A4, A19, WAYBEL_0:66;
hence fx in compactbelow (f . (g . y)) by A20, WAYBEL_8:4; :: thesis: fx is_>=_than Y
Y c= the carrier of L2 by XBOOLE_1:1;
then A21: Y c= rng f by A4, WAYBEL_0:66;
f .: X = f .: (f " Y) by A7, FUNCT_1:155
.= Y by A21, FUNCT_1:147 ;
hence fx is_>=_than Y by A4, A18, 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 A7, A8, FUNCT_1:57; :: thesis: verum

end;

A22: L2 is up-complete by A1, A3, Th30;
L1 is non empty with_suprema lower-bounded up-complete Poset by A2;
then L2 is satisfying_axiom_K by A1, A3, Th31;
hence L2 is algebraic by A6, A22, WAYBEL_8:def 4; :: thesis: verum