c3
有限の補題
word(ss,s) … \(\text{inj}\)inj. … \(\text{inj} _ ( n , k ) = \lceil \bullet \rfloor | _ k \cup \lceil \bullet \textit{+1} \rfloor | _ ( n \mathop\setminus k )\)
inj! … \(k \subset n \in \mathbb{M} \Longrightarrow \text{inj} _ ( n , k ) \in n \stackrel{\rm IS}\to n \textit{+1} \mathop\setminus \{ k \}\)
c4
\(X \times Y \stackrel{\#}= Y \times X\) \(\blacktriangleleft\)\(X \to ( Y \to Z ) \stackrel{\#}= X \times Y \to Z\) \(\blacktriangleleft\)