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

( 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