let X, y be set ; :: thesis: ( X is trivial & not X \/ {y} is trivial implies ex x being set st X = {x} )
assume A1: ( X is trivial & not X \/ {y} is trivial ) ; :: thesis: ex x being set st X = {x}
then ( X is zero or ex x being set st X = {x} ) by REALSET1:def 4;
hence ex x being set st X = {x} by A1; :: thesis: verum