let X be set ; :: thesis: ( not X is empty & X is trivial implies ex x being object st X = {x} )
assume not X is empty ; :: thesis: ( not X is trivial or ex x being object st X = {x} )
then consider x being object such that
A1: x in X ;
assume A2: X is trivial ; :: thesis: ex x being object st X = {x}
take x ; :: thesis: X = {x}
for y being object holds
( y in X iff x = y ) by A2, A1;
hence X = {x} by TARSKI:def 1; :: thesis: verum