for L being non empty lower-bounded Poset
for F being Filter of L holds
( F is proper iff not Bottom L in F )