let F be non trivial set ; :: thesis: for A being OnePoint of F holds F \ A is non empty set
let A be OnePoint of F; :: thesis: F \ A is non empty set
ex x being Element of F st A = {x} by Lm1;
hence F \ A is non empty set by Th4; :: thesis: verum