theorem xpsnd (A B: set) (a: nat): $ a e. Xp A B -> snd a e. B $;
a e. Xp A B <-> fst a e. A /\ snd a e. B
fst a e. A /\ snd a e. B -> snd a e. B
a e. Xp A B -> snd a e. B