consider t being set such that
A1: t in X by XBOOLE_0:def 1;
consider l being set such that
A2: l in L by XBOOLE_0:def 1;
PairSet t,l in PairSetFamily L by A1, A2, Def10;
hence not PairSetFamily L is empty ; :: thesis: verum