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