Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 22 | ∀a: ∀b: ∀c: <(a+c)=(b+c) ⇒ a=b> | |||||||||
| (2) | Spezialisierung (1) a ← d | ∀b: ∀c: <(d+c)=(b+c) ⇒ d=b> | |||||||||
| (3) | Spezialisierung (2) b ← 0 | ∀c: <(d+c)=(0+c) ⇒ d=0> | |||||||||
| (4) | Spezialisierung (3) c ← a | <(d+a)=(0+a) ⇒ d=0> | |||||||||
| (5) | Verallgemeinerung (4) nach d | ∀d: <(d+a)=(0+a) ⇒ d=0> | |||||||||
| (6) | Spezialisierung (5) d ← b | <(b+a)=(0+a) ⇒ b=0> | |||||||||
| (7) | Theorem 5 | ∀a: (0+a)=a | |||||||||
| (8) | Spezialisierung (7) a ← a | (0+a)=a | |||||||||
| (9) | Symmetrie (8) | a=(0+a) | |||||||||
| (10) | Theorem 8 | ∀a: ∀b: (a+b)=(b+a) | |||||||||
| (11) | Spezialisierung (10) a ← a | ∀b: (a+b)=(b+a) | |||||||||
| (12) | Spezialisierung (11) b ← b | (a+b)=(b+a) | |||||||||
| (13) | Symmetrie (12) | (b+a)=(a+b) | |||||||||
| (14) | Hypothese | (a+b)=a | |||||||||
| (15) | Übernahme (13) | (b+a)=(a+b) | |||||||||
| (16) | Transitivität (15), (14) | (b+a)=a | |||||||||
| (17) | Übernahme (9) | a=(0+a) | |||||||||
| (18) | Transitivität (16), (17) | (b+a)=(0+a) | |||||||||
| (19) | Übernahme (6) | <(b+a)=(0+a) ⇒ b=0> | |||||||||
| (20) | Modus ponens (19), (18) | b=0 | |||||||||
| (21) | Konklusion (14), (20) | <(a+b)=a ⇒ b=0> | |||||||||
| (22) | Verallgemeinerung (21) nach b | ∀b: <(a+b)=a ⇒ b=0> | |||||||||
| (23) | Verallgemeinerung (22) nach a | ∀a: ∀b: <(a+b)=a ⇒ b=0> | |||||||||