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

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