theorem Th1: :: YELLOW19:1

for X being non empty set
for F being proper Filter of (BoolePoset X)
for A being set st A in F holds
not A is empty