consider x being object such that
A1: x in X by XBOOLE_0:def 1;
{t,x} in PairSet (t,X) by A1, Def9;
hence not PairSet (t,X) is empty ; :: thesis: verum