let L be 0_Lattice; :: thesis: for F being Filter of L holds
( not F is being_ultrafilter or not Bottom L in F )
given F being Filter of L such that A1: F is being_ultrafilter and
A2: Bottom L in F ; :: thesis: contradiction
F = the carrier of L by A2, FILTER_0:26;
hence contradiction by A1, FILTER_0:def 3; :: thesis: verum