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_{1} being object st

( x in A & b_{1} in A & not x = b_{1} )

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

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

( x in A & 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