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;
A1: Y in F ;
X c= X ;
hence X in F by A1, Def1; :: thesis: verum