let L be lower-bounded LATTICE; ( L is algebraic implies ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic ) )
assume A1:
L is algebraic
; ex X being non empty set ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
then reconsider L9 = L as lower-bounded algebraic LATTICE ;
take X = the carrier of (CompactSublatt L); ex S being full SubRelStr of BoolePoset X st
( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
consider g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) such that
A2:
g is infs-preserving
and
A3:
g is directed-sups-preserving
and
A4:
g is V13()
and
A5:
for x being Element of L holds g . x = compactbelow x
by A1, Th24;
reconsider S = Image g as non empty full SubRelStr of BoolePoset X ;
take
S
; ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )
A6:
L9 is complete
;
hence
S is infs-inheriting
by A2, YELLOW_2:33; ( S is directed-sups-inheriting & L,S are_isomorphic )
A7:
rng g = the carrier of S
by YELLOW_0:def 15;
dom g = the carrier of L
by FUNCT_2:def 1;
then reconsider g1 = g as Function of L,S by A7, FUNCT_2:1;
now for x, y being Element of L holds
( ( x <= y implies g1 . x <= g1 . y ) & ( g1 . x <= g1 . y implies x <= y ) )let x,
y be
Element of
L;
( ( x <= y implies g1 . x <= g1 . y ) & ( g1 . x <= g1 . y implies x <= y ) )thus
(
x <= y implies
g1 . x <= g1 . y )
( g1 . x <= g1 . y implies x <= y )thus
(
g1 . x <= g1 . y implies
x <= y )
verum end;
then A9:
g1 is isomorphic
by A4, A7, WAYBEL_0:66;
then reconsider f1 = g1 " as Function of S,L by WAYBEL_0:67;
A10:
f1 is isomorphic
by A9, WAYBEL_0:68;
now for Y being directed Subset of S st Y <> {} & ex_sup_of Y, BoolePoset X holds
"\/" (Y,(BoolePoset X)) in the carrier of Slet Y be
directed Subset of
S;
( Y <> {} & ex_sup_of Y, BoolePoset X implies "\/" (Y,(BoolePoset X)) in the carrier of S )assume that A11:
Y <> {}
and
ex_sup_of Y,
BoolePoset X
;
"\/" (Y,(BoolePoset X)) in the carrier of Sthen reconsider X1 =
f1 .: Y as non
empty directed Subset of
L by WAYBEL_0:1;
sup X1 in the
carrier of
L
;
then
sup X1 in dom g
by FUNCT_2:def 1;
then A16:
g . (sup X1) in rng g
by FUNCT_1:def 3;
(
ex_sup_of X1,
L &
g preserves_sup_of X1 )
by A6, A3, WAYBEL_0:def 37, YELLOW_0:17;
then A17:
sup (g .: X1) in rng g
by A16, WAYBEL_0:def 31;
g .: X1 =
g .: (g1 " Y)
by A4, FUNCT_1:85
.=
Y
by A7, FUNCT_1:77
;
hence
"\/" (
Y,
(BoolePoset X))
in the
carrier of
S
by A17, YELLOW_0:def 15;
verum end;
hence
S is directed-sups-inheriting
by WAYBEL_0:def 4; L,S are_isomorphic
thus
L,S are_isomorphic
by A9, WAYBEL_1:def 8; verum