how to deduce a function subtype rule from a given function type definition
The intersection rule should be derivable, but it isn't purely a subtyping rule. Basically we reason as follows (I've translated into a notation that's a bit more familiar to me):


I'm presuming that subtyping says $A \cap B \subseteq A \subseteq A \cup B$
Subtyping means that $f : (A \to Y) \cap (B \to X)$ leads to both $f : A \to Y$ and $f : B \to X$
If $f : A \to Y$, it is then the case that $x : A ⊢ f \; x : Y$. But subtyping $A \cap B \subseteq A$ means that $x : A \cap B ⊢ f \; x : Y$ follows.
The same argument means that $f : B \to X$ leads to $x : A \cap B ⊢ f \; x : X$
These two judgments together lead to $x : A \cap B ⊢ f \; x : X \cap Y$
This leads back to $f : A \cap B \to X \cap Y$


Another way to specify this is that $f : (A \to X) \cap (A \to Y)$ leads to $f : A \to X \cap Y$. Subtyping allows us to broaden the original $A$ and $B$ to the common $A \cap B$, and then apply this intersection rule. But the intersection rule isn't subtyping, it is the rule for deducing that something has an intersection type via two separate deductions.

Pure subtyping can allow you to go from $f : A \to Y$ to $f : A \cap B \to X \cup Y$. Note that this is refining the input and broadening the output, and we could do each individually.

For union types, there is an opposite sort of rule. $f : (A \to Y) \cap (B \to Y)$ leads to $f : A \cup B \to Y$. So, if you can map both $A$ values and $B$ values to $Y$ values, you can map their union to $Y$ values. However, note that this doesn't allow us to deduce your rule with a union. Instead, we can only get from $f : (A \to Y) \cap (B \to X)$ to $f : A \cup B \to X \cup Y$, because this time we can broaden the result type of both functions and apply the union rule.

But, there is no way (I think) to get to $f : A \cup B \to X \cap Y$, which makes sense if you think about it. Just because we know that $f$ takes $A$ values to $Y$ values and $B$ values to $X$ values doesn't imply that it takes all $B$ values to $Y$ values and $A$ values to $X$ values, which is what that specification says.

So, to sum up:


The rule is derivable (with some standard assumptions, I think).
The rule is not a contradiction.
We can derive a union rule, but not the one you wrote. And I'm unsure what 'complement' rule you're talking about.
Subtyping works as usual, but it is not the only basis for the intersection/union rules.


Edit: Here's a summary of the rules that I believe hold, as I think it might lead you less astray than the long stuff above:

$$(A \to Y) \cap (B \to X) \subseteq (A \cap B) \to (X \cap Y)$$
$$(A \to Y) \cap (B \to Y) \cong A \cup B \to Y$$
$$(A \to X) \cap (A \to Y) \cong A \to X \cap Y$$

In particular, note that the first relationship is subtyping, not equivalence. The intersection of the function types carries more information than the function between intersection types. If the lisp documentation you're looking at says those are the same, it's wrong. Consider, just because we know that a function takes $A \cap B$ to $X \cap Y$ doesn't tell us anything about what it takes $A - B$ to. However, if it's merely saying that knowing $f$ has the first two types, we can conclude it also has the third type, that is correct.