for L being Lattice st L is lower-bounded holds
for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter )