Es gelten die allgemeinen Vorbemerkungen.
(1) | Hypothese | ∀b: ¬(a·Sb)=a | |||||||||
(2) | Spezialisierung (1) b ← 0 | ¬(a·S0)=a | |||||||||
(3) | Konklusion (1), (2) | <∀b: ¬(a·Sb)=a ⇒ ¬(a·S0)=a> | |||||||||
(4) | Kontraposition (3) | <¬¬(a·S0)=a ⇒ ¬∀b: ¬(a·Sb)=a> | |||||||||
(5) | Theorem 25 | ∀a: (a·S0)=a | |||||||||
(6) | Spezialisierung (5) a ← a | (a·S0)=a | |||||||||
(7) | Doppelte Negation (6) | ¬¬(a·S0)=a | |||||||||
(8) | Modus ponens (4), (7) | ¬∀b: ¬(a·Sb)=a | |||||||||
(9) | Verallgemeinerung (8) nach a | ∀a: ¬∀b: ¬(a·Sb)=a |
Interpretation:
'teilt' ist reflexiv