theorem nfxp {x: nat} (A B: set x): $ FS/ x A $ > $ FS/ x B $ > $ FS/ x Xp A B $;
FS/ x A
FS/ x B
FS/ x X\ y e. A, B
FS/ x Xp A B