2 c= card X by PENCIL_1:4;
then consider x, y being set such that
A1: ( x in X & y in X ) and
A2: x <> y by PENCIL_1:2;

A3: now

assume A4: {t,x} = {t,y} ; :: thesis: contradiction
then y = t by A2, ZFMISC_1:10;
hence contradiction by A2, A4, ZFMISC_1:10; :: thesis: verum

end;

( {t,x} in PairSet t,X & {t,y} in PairSet t,X ) by A1, Def9;
then 2 c= card (PairSet t,X) by A3, PENCIL_1:2;
hence not PairSet t,X is trivial by PENCIL_1:4; :: thesis: verum