let X be non empty set ; :: thesis: ( not X is trivial iff for x being set holds X \ {x} is non empty set )

hereby :: thesis: ( ( for x being set holds X \ {x} is non empty set ) implies not X is trivial )

assume A1: not X is trivial ; :: thesis: for x being set holds X \ {x} is non empty set
let x be set ; :: thesis: X \ {x} is non empty set
X <> {x} by A1;
then consider y being set such that
A2: y in X and
A3: x <> y by ZFMISC_1:41;
not y in {x} by A3, TARSKI:def 1;
hence X \ {x} is non empty set by A2, XBOOLE_0:def 5; :: thesis: verum

end;

assume A4: for x being set holds X \ {x} is non empty set ; :: thesis: not X is trivial
thus not X is empty ; :: according to REALSET1:def 4 :: thesis: for x being set holds not X = {x}
given x being set such that A5: X = {x} ; :: thesis: contradiction
X \ {x} is empty by A5, XBOOLE_1:37;
hence contradiction by A4; :: thesis: verum