let L be lower-bounded continuous LATTICE; :: thesis: ( 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 ; :: thesis: L is algebraic
A2: [(supMap (subrelstr B)),(baseMap B)] is Galois by Th63;
A3: rng (supMap (subrelstr B)) = the carrier of L by Th65;
the carrier of (InclPoset (Ids (subrelstr B))) c= rng (baseMap B)

proof

let J be set ; :: according to TARSKI:def 3 :: thesis: ( not J in the carrier of (InclPoset (Ids (subrelstr B))) or J in rng (baseMap B) )
assume A4: J in the carrier of (InclPoset (Ids (subrelstr B))) ; :: thesis: J in rng (baseMap B)
set x = "\/" J,L;
J = (waybelow ("\/" J,L)) /\ B by A1, A4, Th71;
then A5: J = (baseMap B) . ("\/" J,L) by Def12;
dom (baseMap B) = the carrier of L by FUNCT_2:def 1;
hence J in rng (baseMap B) by A5, FUNCT_1:def 5; :: thesis: verum

end;

then rng (baseMap B) = the carrier of (InclPoset (Ids (subrelstr B))) by XBOOLE_0:def 10;
then baseMap B is onto by FUNCT_2:def 3;
then A6: supMap (subrelstr B) is one-to-one by A2, WAYBEL_1:29;
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))); :: thesis: ( 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; :: thesis: ( (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y implies x <= y )
reconsider x1 = x, y1 = y as Ideal of (subrelstr B) by YELLOW_2:43;
A7: ( (supMap (subrelstr B)) . x1 = "\/" x1,L & (supMap (subrelstr B)) . y1 = "\/" y1,L ) by Def10;
A8: ( x = (waybelow ("\/" x,L)) /\ B & y = (waybelow ("\/" y,L)) /\ B ) by A1, Th71;
assume (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ; :: thesis: x <= y
then waybelow ("\/" x1,L) c= waybelow ("\/" y1,L) by A7, WAYBEL_3:25;
then (waybelow ("\/" x1,L)) /\ B c= (waybelow ("\/" y1,L)) /\ B by XBOOLE_1:26;
hence x <= y by A8, YELLOW_1:3; :: thesis: verum

end;

then supMap (subrelstr B) is isomorphic by A3, A6, WAYBEL_0:66;
then A9: 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 A9, WAYBEL13:32; :: thesis: verum