let X be non empty set ; :: thesis:
let F be Filter of X; :: thesis:
let I be non empty Subset-Family of X; :: thesis:
assume A1: for Y being Subset of X holds
( Y in I iff Y ` in F ) ; :: thesis:
not (({} X) `) ` in F by Def1;
hence not X in I by A1; :: thesis:
let Y1, Y2 be Subset of X; :: thesis:
thus ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) :: thesis:

assume ( Y1 in I & Y2 in I ) ; :: thesis:
then ( Y1 ` in F & Y2 ` in F ) by A1;
then (Y1 `) /\ (Y2 `) in F by Def1;
then (Y1 \/ Y2) ` in F by XBOOLE_1:53;
hence Y1 \/ Y2 in I by A1; :: thesis:

end;