let L1, L2 be sup-Semilattice; ( 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 )
; 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 for y being Element of L2 holds
( not compactbelow y is empty & compactbelow y is directed )let y be
Element of
L2;
( 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 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)));
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;
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;
( 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;
fx is_>=_than Yf .: X =
f .: (f " Y)
by A3, FUNCT_1:85
.=
Y
by A9, FUNCT_1:77
;
hence
fx is_>=_than Y
by A3, A15, Th19;
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;
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; verum