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>> |