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
set Y = the Element of F;
( the Element of F in F & X c= X ) ;
hence X in F by Def1; :: thesis: verum