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