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