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

now

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

end;

then 2 c= card (PairSet t,X) by A2, PENCIL_1:2;
hence not PairSet t,X is trivial by PENCIL_1:4; :: thesis: verum