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
A1: x in X by XBOOLE_0:def 1;
assume A2: X is trivial ; :: thesis: ex x being set st X = {x}
take x ; :: thesis: X = {x}
for y being set holds
( y in X iff x = y ) by A2, A1, Def10;
hence X = {x} by TARSKI:def 1; :: thesis: verum