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