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 & Bottom L in F ) ; :: thesis: contradiction
( F = <.L.) & F = the carrier of L ) by A1, FILTER_0:32;
hence contradiction by A1, FILTER_0:def 4; :: thesis: verum