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:43;
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, Th71;
x = (waybelow ("\/" x,L)) /\ B by A1, Th71;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not J in the carrier of (InclPoset (Ids (subrelstr B))) or J in rng (baseMap B) )
set x = "\/" J,L;
assume J in the carrier of (InclPoset (Ids (subrelstr B))) ; :: thesis: J in rng (baseMap B)
then J = (waybelow ("\/" J,L)) /\ B by A1, Th71;
then A7: 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 A7, FUNCT_1:def 5; :: thesis: verum

end;

then rng (baseMap B) = the carrier of (InclPoset (Ids (subrelstr B))) by XBOOLE_0:def 10;
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:29;
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