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