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