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