let F be non trivial set ; :: thesis: for A being OnePoint of F ex x being Element of F st A = {x}
let A be OnePoint of F; :: thesis: ex x being Element of F st A = {x}
consider x being set such that
A1: A = {x} by Def4;
x in A by A1, TARSKI:def 1;
hence ex x being Element of F st A = {x} by A1; :: thesis: verum