theorem prelxp1 (A B: set) (a b: nat): $ a, b e. Xp A B -> a e. A $;
a, b e. Xp A B <-> a e. A /\ b e. B
a e. A /\ b e. B -> a e. A
a, b e. Xp A B -> a e. A