let X be 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 A1, ZFMISC_1:35;
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
X \ {{}} c= X ;
then not X is empty by A4;
then consider x being set such that
W1: x in X by XBOOLE_0:def 1;
not X \ {x} is empty by A4;
then consider y being set such that
W2: y in X \ {x} by XBOOLE_0:def 1;
take x ; :: according to ZFMISC_1:def 10 :: thesis: ex b₁ being set st
( x in X & b₁ in X & not x = b₁ )
take y ; :: thesis: ( x in X & y in X & not x = y )
thus x in X by W1; :: thesis: ( y in X & not x = y )
thus y in X by W2; :: thesis: not x = y
x in {x} by TARSKI:def 1;
then not x in X \ {x} by XBOOLE_0:def 5;
hence x <> y by W2; :: thesis: verum