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

proof

assume ( Y1 in I & Y2 in I ) ; :: thesis: Y1 \/ Y2 in I
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: verum

end;

assume A2: ( Y1 in I & Y2 c= Y1 ) ; :: thesis: Y2 in I
then A3: Y1 ` in F by A1;
Y1 ` c= Y2 ` by A2, SUBSET_1:31;
then Y2 ` in F by A3, Def1;
hence Y2 in I by A1; :: thesis: verum