Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (2) | Spezialisierung (1) a ← a | (a+0)=a | |||||||||
| (3) | Hypothese | ∀d: ¬(a+d)=a | |||||||||
| (4) | Spezialisierung (3) d ← 0 | ¬(a+0)=a | |||||||||
| (5) | Konklusion (3), (4) | <∀d: ¬(a+d)=a ⇒ ¬(a+0)=a> | |||||||||
| (6) | Kontraposition (5) | <¬¬(a+0)=a ⇒ ¬∀d: ¬(a+d)=a> | |||||||||
| (7) | Doppelte Negation (2) | ¬¬(a+0)=a | |||||||||
| (8) | Modus ponens (6), (7) | ¬∀d: ¬(a+d)=a | |||||||||
| (9) | Verallgemeinerung (8) nach a | ∀a: ¬∀d: ¬(a+d)=a | |||||||||
Interpretation:
≤ ist reflexiv