thus ( not IT is trivial or IT is empty or ex x being set st IT = {x} ) :: thesis: ( ( IT is empty or ex x being set st IT = {x} ) implies IT is trivial )

proof

assume A1: IT is trivial ; :: thesis: ( IT is empty or ex x being set st IT = {x} )
assume not IT is empty ; :: thesis: ex x being set st IT = {x}
then consider x being set such that
A2: x in IT by XBOOLE_0:def 1;
take x ; :: thesis: IT = {x}
for y being set holds
( y in IT iff y = x ) by A1, A2, ZFMISC_1:def 10;
hence IT = {x} by TARSKI:def 1; :: thesis: verum

end;

assume A3: ( IT is empty or ex x being set st IT = {x} ) ; :: thesis: IT is trivial
assume A4: not IT is trivial ; :: thesis: contradiction
then consider x0 being set such that
A5: IT = {x0} by A3;

now

let x, y be set ; :: thesis: ( x in IT & y in IT implies x = y )
assume that
A6: x in IT and
A7: y in IT ; :: thesis: x = y
thus x = x0 by A5, A6, TARSKI:def 1
.= y by A5, A7, TARSKI:def 1 ; :: thesis: verum

end;

hence contradiction by A4, ZFMISC_1:def 10; :: thesis: verum