theorem Th7: :: CARD_FIL:7

for X being non empty set
for F being Filter of X
for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )