let F be Filter of L; :: thesis: ( F is being_ultrafilter implies F is maximal )
assume a0: F is being_ultrafilter ; :: thesis: F is maximal
then A0: ( F <> the carrier of L & ( for H being Filter of L st F c= H & H <> the carrier of L holds
F = H ) ) by FILTER_0:def 3;
for G being Filter of L st G is proper & F c= G holds
F = G

proof

let G be Filter of L; :: thesis: ( G is proper & F c= G implies F = G )
assume A2: ( G is proper & F c= G ) ; :: thesis: F = G
then G <> the carrier of L by SUBSET_1:def 6;
hence F = G by a0, A2, FILTER_0:def 3; :: thesis: verum

end;

hence F is maximal by A0, SUBSET_1:def 6; :: thesis: verum