consider x, y being Element of T such that
A1: x <> y by Def10;
reconsider A = {x,y} as Subset of T ;
take A ; :: thesis: not A is trivial
take x ; :: according to ZFMISC_1:def 10 :: thesis: ex b₁ being object st
( x in A & b₁ in A & not x = b₁ )
take y ; :: thesis: ( x in A & y in A & not x = y )
thus x in A by TARSKI:def 2; :: thesis: ( y in A & not x = y )
thus y in A by TARSKI:def 2; :: thesis: not x = y
thus not x = y by A1; :: thesis: verum