let H be non trivial H_Lattice; :: thesis: (StoneH H) . (Bottom H) = {}
set x = the Element of (StoneH H) . (Bottom H);
assume (StoneH H) . (Bottom H) <> {} ; :: thesis: contradiction
then ex F being Filter of H st
( F = the Element of (StoneH H) . (Bottom H) & F <> the carrier of H & F is prime & Bottom H in F ) by Th12;
hence contradiction by FILTER_0:26; :: thesis: verum