the Element of X in X by Def2;
then { the Element of X} c= X by ZFMISC_1:31;
then { the Element of X} in bool X by ZFMISC_1:def 1;
then reconsider A = { the Element of X} as Subset of X by Def2;
take A ; :: thesis: ( not A is empty & A is trivial )
thus not A is empty ; :: thesis: A is trivial
let x, y be set ; :: according to ZFMISC_1:def 10 :: thesis: ( not x in A or not y in A or x = y )
assume ( x in A & y in A ) ; :: thesis: x = y
then ( x = the Element of X & y = the Element of X ) by TARSKI:def 1;
hence x = y ; :: thesis: verum