theorem Th35: :: CARDFIL2:75

for X being non empty set
for F being non empty Subset of (BooleLatt X) holds
( ( F is with_non-empty_elements & F is Filter of (BooleLatt X) ) iff F is Filter of X )