Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 5 | ∀a: (0+a)=a | |||||||||
| (2) | Spezialisierung (1) a ← b | (0+b)=b | |||||||||
| (3) | Hypothese | ∀c: ¬(0+c)=b | |||||||||
| (4) | Spezialisierung (3) c ← b | ¬(0+b)=b | |||||||||
| (5) | Konklusion (3), (4) | <∀c: ¬(0+c)=b ⇒ ¬(0+b)=b> | |||||||||
| (6) | Kontraposition (5) | <¬¬(0+b)=b ⇒ ¬∀c: ¬(0+c)=b> | |||||||||
| (7) | Doppelte Negation (2) | ¬¬(0+b)=b | |||||||||
| (8) | Modus ponens (6), (7) | ¬∀c: ¬(0+c)=b | |||||||||
| (9) | Hypothese | ∀c: ¬(0+c)=b | |||||||||
| (10) | Hypothese | ∀c: ¬(b+c)=0 | |||||||||
| (11) | Übernahme (8) | ¬∀c: ¬(0+c)=b | |||||||||
| (12) | Konklusion (10), (11) | <∀c: ¬(b+c)=0 ⇒ ¬∀c: ¬(0+c)=b> | |||||||||
| (13) | Kontraposition (12) | <¬¬∀c: ¬(0+c)=b ⇒ ¬∀c: ¬(b+c)=0> | |||||||||
| (14) | Doppelte Negation (9) | ¬¬∀c: ¬(0+c)=b | |||||||||
| (15) | Modus ponens (13), (14) | ¬∀c: ¬(b+c)=0 | |||||||||
| (16) | Konklusion (9), (15) | <∀c: ¬(0+c)=b ⇒ ¬∀c: ¬(b+c)=0> | |||||||||
| (17) | Verallgemeinerung (16) nach b | ∀b: <∀c: ¬(0+c)=b ⇒ ¬∀c: ¬(b+c)=0> | |||||||||
Interpretation:
≤ ist bei 0 eine Totalordnung