2 c= card X by PENCIL_1:4;
then consider x, y being object such that
A1: ( x in X & y in X ) and
A2: x <> y by PENCIL_1:2;
A3: now :: thesis: not {t,x} = {t,y}
assume A4: {t,x} = {t,y} ; :: thesis: contradiction
then y = t by A2, ZFMISC_1:6;
hence contradiction by A2, A4, ZFMISC_1:6; :: 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