theorem Th31: :: CARDFIL2:71

for X being non empty set
for F being non empty Subset of (BooleLatt X) holds
( F is Filter of (BooleLatt X) iff ( ( for p, q being Element of F holds p /\ q in F ) & ( for p being Element of F
for q being Element of (BooleLatt X) st p c= q holds
q in F ) ) )