let X, y be set ; :: thesis: ( X is trivial & not X \/ {y} is trivial implies ex x being object st X = {x} )
assume that
A1: X is trivial and
A2: not X \/ {y} is trivial ; :: thesis: ex x being object st X = {x}
( X is empty or ex x being object st X = {x} ) by A1, ZFMISC_1:131;
hence ex x being object st X = {x} by A2; :: thesis: verum