Es gelten die allgemeinen Vorbemerkungen.
| (1) | Hypothese | ∀e: ∀f: <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> | |||||||||
| (2) | Spezialisierung (1) e ← e | ∀f: <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> | |||||||||
| (3) | Spezialisierung (2) f ← f | <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> | |||||||||
| (4) | Kontraposition (3) | <¬(a+(e+f))=c ⇒ ¬<(a+e)=b∧(b+f)=c>> | |||||||||
| (5) | Hypothese | ∀e: ∀f: ¬(a+(e+f))=c | |||||||||
| (6) | Spezialisierung (5) e ← e | ∀f: ¬(a+(e+f))=c | |||||||||
| (7) | Spezialisierung (6) f ← f | ¬(a+(e+f))=c | |||||||||
| (8) | Übernahme (4) | <¬(a+(e+f))=c ⇒ ¬<(a+e)=b∧(b+f)=c>> | |||||||||
| (9) | Modus ponens (8), (7) | ¬<(a+e)=b∧(b+f)=c> | |||||||||
| (10) | Verallgemeinerung (9) nach f | ∀f: ¬<(a+e)=b∧(b+f)=c> | |||||||||
| (11) | Verallgemeinerung (10) nach e | ∀e: ∀f: ¬<(a+e)=b∧(b+f)=c> | |||||||||
| (12) | Konklusion (5), (11) | <∀e: ∀f: ¬(a+(e+f))=c ⇒ ∀e: ∀f: ¬<(a+e)=b∧(b+f)=c>> | |||||||||
| (13) | Kontraposition (12) | <¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c> ⇒ ¬∀e: ∀f: ¬(a+(e+f))=c> | |||||||||
| (14) | Konklusion (1), (13) | <∀e: ∀f: <<(a+e)=b∧(b+f)=c> ⇒ (a+(e+f))=c> ⇒ <¬∀e: ∀f: ¬<(a+e)=b∧(b+f)=c> ⇒ ¬∀e: ∀f: ¬(a+(e+f))=c>> | |||||||||