let H be non trivial H_Lattice; :: thesis: (StoneH H) . (Bottom H) = {}
assume A1: (StoneH H) . (Bottom H) <> {} ; :: thesis: contradiction
consider x being Element of (StoneH H) . (Bottom H);
consider F being Filter of H such that
A2: ( F = x & F <> the carrier of H & F is prime & Bottom H in F ) by A1, Th14;
thus contradiction by A2, FILTER_0:32; :: thesis: verum