let F be Filter of L; :: thesis: ( F is maximal implies F is being_ultrafilter )
assume a0: F is maximal ; :: thesis: F is being_ultrafilter
for H being Filter of L st F c= H & H <> the carrier of L holds
F = H

proof

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

end;

hence F is being_ultrafilter by a0, SUBSET_1:def 6, FILTER_0:def 3; :: thesis: verum