let X be set ; :: thesis: ( not X is trivial iff for x being object holds not X \ {x} is empty )
hereby :: thesis: ( ( for x being object holds not X \ {x} is empty ) implies not X is trivial )
assume A1: not X is trivial ; :: thesis: for x being object holds not X \ {x} is empty
let x be object ; :: thesis: not X \ {x} is empty
X <> {x} by A1;
then consider y being object such that
A2: y in X and
A3: x <> y by A1, Lm12;
not y in {x} by A3, TARSKI:def 1;
hence not X \ {x} is empty by A2, XBOOLE_0:def 5; :: thesis: verum
end;
assume A4: for x being object holds not X \ {x} is empty ; :: thesis: not X is trivial
X \ {{}} c= X by XBOOLE_1:36;
then not X is empty by A4;
then consider x being object such that
A5: x in X ;
not X \ {x} is empty by A4;
then consider y being object such that
A6: y in X \ {x} ;
reconsider x = x, y = y as set by TARSKI:1;
take x ; :: according to ZFMISC_1:def 10 :: thesis: ex y being object st
( x in X & y in X & not x = y )
take y ; :: thesis: ( x in X & y in X & not x = y )
thus x in X by A5; :: thesis: ( y in X & not x = y )
X \ {x} c= X by XBOOLE_1:36;
hence y in X by A6; :: thesis: not x = y
x in {x} by TARSKI:def 1;
hence x <> y by A6, XBOOLE_0:def 5; :: thesis: verum