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:8; :: thesis: verum