let X be non empty set ; :: thesis: for F being proper Filter of (BoolePoset X)
for A being set st A in F holds
not A is empty
Bottom (BoolePoset X) = {} by YELLOW_1:18;
hence for F being proper Filter of (BoolePoset X)
for A being set st A in F holds
not A is empty by WAYBEL_7:4; :: thesis: verum