theorem Th32: :: CARDFIL2:72

for X being non empty set
for F being non empty Subset of (BooleLatt X) holds
( F is Filter of (BooleLatt X) iff for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) )