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 Z: 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
W: 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 Z, W, ZFMISC_1:def 10;
hence IT = {x} by TARSKI:def 1; :: thesis: verum

end;

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

now

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

end;

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