let X be non empty set ; :: thesis: for F being Filter of X holds X in F
let F be Filter of X; :: thesis: X in F
consider Y being Element of F;
( Y in F & X c= X ) ;
hence X in F by Def1; :: thesis: verum