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

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