set p = Bottom L;
Bottom L <> Top L by TopBot;
then consider I being Ideal of L such that
A0: ( Bottom L in I & I is max-ideal ) by FILTER_2:35;
a2: I <> the carrier of L by FILTER_2:def 8, A0;
for G being Ideal of L st G is proper & I c= G holds
I = G

proof

let G be Ideal of L; :: thesis: ( G is proper & I c= G implies I = G )
assume B1: ( G is proper & I c= G ) ; :: thesis: I = G
then G <> the carrier of L by SUBSET_1:def 6;
hence I = G by FILTER_2:def 8, A0, B1; :: thesis: verum

end;

then I is maximal by a2, SUBSET_1:def 6;
then I in Spectrum L ;
hence not Spectrum L is empty ; :: thesis: verum