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 )

A2: Y1 in I and

A3: Y2 c= Y1 ; :: thesis: Y2 in I

A4: Y1 ` c= Y2 ` by A3, SUBSET_1:12;

Y1 ` in F by A1, A2;

then Y2 ` in F by A4, Def1;

hence Y2 in I by A1; :: thesis: verum

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 that
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;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

A2: Y1 in I and

A3: Y2 c= Y1 ; :: thesis: Y2 in I

A4: Y1 ` c= Y2 ` by A3, SUBSET_1:12;

Y1 ` in F by A1, A2;

then Y2 ` in F by A4, Def1;

hence Y2 in I by A1; :: thesis: verum