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: 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:41;
assume A3: (supMap (subrelstr B)) . x <= (supMap (subrelstr B)) . y ; :: thesis: 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; :: thesis: verum

end;

the carrier of (InclPoset (Ids (subrelstr B))) c= rng (baseMap B)

proof

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

end;

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 one-to-one 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; :: thesis: verum