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

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