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