let L be lower-bounded continuous LATTICE; ( ex B being with_bottom CLbasis of L st
for B1 being with_bottom CLbasis of L holds B c= B1 implies L is algebraic )
given B being with_bottom CLbasis of L such that A1:
for B1 being with_bottom CLbasis of L holds B c= B1
; L is algebraic
A2:
for x, y being Element of (InclPoset (Ids (subrelstr B))) holds
( x <= y iff (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )
proof
let x,
y be
Element of
(InclPoset (Ids (subrelstr B)));
( x <= y iff (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )
thus
(
x <= y implies
(supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y )
by WAYBEL_1:def 2;
( (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y implies x <= y )
reconsider x1 =
x,
y1 =
y as
Ideal of
(subrelstr B) by YELLOW_2:41;
assume A3:
(supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y
;
x <= y
A4:
(supMap (subrelstr B)) . y1 = "\/" (
y1,
L)
by Def10;
(supMap (subrelstr B)) . x1 = "\/" (
x1,
L)
by Def10;
then
waybelow ("\/" (x1,L)) c= waybelow ("\/" (y1,L))
by A4, A3, WAYBEL_3:25;
then A5:
(waybelow ("\/" (x1,L))) /\ B c= (waybelow ("\/" (y1,L))) /\ B
by XBOOLE_1:26;
A6:
y = (waybelow ("\/" (y,L))) /\ B
by A1, Th70;
x = (waybelow ("\/" (x,L))) /\ B
by A1, Th70;
hence
x <= y
by A6, A5, YELLOW_1:3;
verum
end;
the carrier of (InclPoset (Ids (subrelstr B))) c= rng (baseMap B)
then
rng (baseMap B) = the carrier of (InclPoset (Ids (subrelstr B)))
;
then A8:
baseMap B is onto
by FUNCT_2:def 3;
[(supMap (subrelstr B)),(baseMap B)] is Galois
by Th63;
then A9:
supMap (subrelstr B) is V13()
by A8, WAYBEL_1:27;
rng (supMap (subrelstr B)) = the carrier of L
by Th65;
then
supMap (subrelstr B) is isomorphic
by A9, A2, WAYBEL_0:66;
then A10:
InclPoset (Ids (subrelstr B)),L are_isomorphic
by WAYBEL_1:def 8;
( InclPoset (Ids (subrelstr B)) is lower-bounded & InclPoset (Ids (subrelstr B)) is algebraic )
by WAYBEL13:10;
hence
L is algebraic
by A10, WAYBEL13:32; verum