let X be non empty set ; :: thesis: ( ( for x being Element of X holds X \ {x} is non empty set ) implies not X is trivial )
assume A1: for x being Element of X 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 A2: X = {x} ; :: thesis: contradiction
( x in X & X \ {x} is empty ) by A2, TARSKI:def 1, XBOOLE_1:37;
hence contradiction by A1; :: thesis: verum