let X be non empty set ; :: thesis: for A being Singleton of X ex x being Element of X st A = {x}
let A be Singleton of X; :: thesis: ex x being Element of X st A = {x}
consider x being object such that
A1: A = {x} by ZFMISC_1:131;
x in A by A1, TARSKI:def 1;
then reconsider x = x as Element of X ;
take x ; :: thesis: A = {x}
thus A = {x} by A1; :: thesis: verum