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 ())) holds
( x <= y iff (supMap ()) . x <= (supMap ()) . y )
proof
let x, y be Element of (InclPoset (Ids ())); :: thesis: ( x <= y iff (supMap ()) . x <= (supMap ()) . y )
thus ( x <= y implies (supMap ()) . x <= (supMap ()) . y ) by WAYBEL_1:def 2; :: thesis: ( (supMap ()) . x <= (supMap ()) . y implies x <= y )
reconsider x1 = x, y1 = y as Ideal of () by YELLOW_2:41;
assume A3: (supMap ()) . x <= (supMap ()) . y ; :: thesis: x <= y
A4: (supMap ()) . y1 = "\/" (y1,L) by Def10;
(supMap ()) . x1 = "\/" (x1,L) by Def10;
then waybelow ("\/" (x1,L)) c= waybelow ("\/" (y1,L)) by ;
then A5: (waybelow ("\/" (x1,L))) /\ B c= (waybelow ("\/" (y1,L))) /\ B by XBOOLE_1:26;
A6: y = (waybelow ("\/" (y,L))) /\ B by ;
x = (waybelow ("\/" (x,L))) /\ B by ;
hence x <= y by ; :: thesis: verum
end;
the carrier of (InclPoset (Ids ())) c= rng ()
proof
let J be object ; :: according to TARSKI:def 3 :: thesis: ( not J in the carrier of (InclPoset (Ids ())) or J in rng () )
reconsider JJ = J as set by TARSKI:1;
set x = "\/" (JJ,L);
assume J in the carrier of (InclPoset (Ids ())) ; :: thesis: J in rng ()
then J = (waybelow ("\/" (JJ,L))) /\ B by ;
then A7: J = () . ("\/" (JJ,L)) by Def12;
dom () = the carrier of L by FUNCT_2:def 1;
hence J in rng () by ; :: thesis: verum
end;
then rng () = the carrier of (InclPoset (Ids ())) ;
then A8: baseMap B is onto by FUNCT_2:def 3;
[(supMap ()),()] is Galois by Th63;
then A9: supMap () is V13() by ;
rng (supMap ()) = the carrier of L by Th65;
then supMap () is isomorphic by ;
then A10: InclPoset (Ids ()),L are_isomorphic by WAYBEL_1:def 8;
( InclPoset (Ids ()) is lower-bounded & InclPoset (Ids ()) is algebraic ) by WAYBEL13:10;
hence L is algebraic by ; :: thesis: verum