let X be set ; :: thesis: ( not X is empty & X is trivial implies ex x being set st X = {x} )
assume not X is empty ; :: thesis: ( not X is trivial or ex x being set st X = {x} )
then consider x being set such that
A: x in X by XBOOLE_0:def 1;
assume Z: X is trivial ; :: thesis: ex x being set st X = {x}
take x ; :: thesis: X = {x}

now

let y be set ; :: thesis: ( y in X iff x = y )
thus ( y in X iff x = y ) by Z, A, Def10; :: thesis: verum

end;

hence X = {x} by TARSKI:def 1; :: thesis: verum