Es gelten die allgemeinen Vorbemerkungen.
| (1) | Hypothese | ∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c> | |||||||||
| (2) | Spezialisierung (1) e ← e | ∀f: ¬<(a·Se)=b∧(b·Sf)=c> | |||||||||
| (3) | Spezialisierung (2) f ← f | ¬<(a·Se)=b∧(b·Sf)=c> | |||||||||
| (4) | Hypothese | (a·Se)=b | |||||||||
| (5) | Hypothese | (b·Sf)=c | |||||||||
| (6) | Übernahme (4) | (a·Se)=b | |||||||||
| (7) | Konjunktion (6), (5) | <(a·Se)=b∧(b·Sf)=c> | |||||||||
| (8) | Konklusion (5), (7) | <(b·Sf)=c ⇒ <(a·Se)=b∧(b·Sf)=c>> | |||||||||
| (9) | Kontraposition (8) | <¬<(a·Se)=b∧(b·Sf)=c> ⇒ ¬(b·Sf)=c> | |||||||||
| (10) | Übernahme (3) | ¬<(a·Se)=b∧(b·Sf)=c> | |||||||||
| (11) | Modus ponens (9), (10) | ¬(b·Sf)=c | |||||||||
| (12) | Verallgemeinerung (11) nach f | ∀f: ¬(b·Sf)=c | |||||||||
| (13) | Konklusion (4), (12) | <(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> | |||||||||
| (14) | Kontraposition (13) | <¬∀f: ¬(b·Sf)=c ⇒ ¬(a·Se)=b> | |||||||||
| (15) | Hypothese | ¬∀f: ¬(b·Sf)=c | |||||||||
| (16) | Übernahme (14) | <¬∀f: ¬(b·Sf)=c ⇒ ¬(a·Se)=b> | |||||||||
| (17) | Modus ponens (16), (15) | ¬(a·Se)=b | |||||||||
| (18) | Verallgemeinerung (17) nach e | ∀e: ¬(a·Se)=b | |||||||||
| (19) | Konklusion (15), (18) | <¬∀f: ¬(b·Sf)=c ⇒ ∀e: ¬(a·Se)=b> | |||||||||
| (20) | Kontraposition (19) | <¬∀e: ¬(a·Se)=b ⇒ ¬¬∀f: ¬(b·Sf)=c> | |||||||||
| (21) | Hypothese | ¬∀e: ¬(a·Se)=b | |||||||||
| (22) | Übernahme (20) | <¬∀e: ¬(a·Se)=b ⇒ ¬¬∀f: ¬(b·Sf)=c> | |||||||||
| (23) | Modus ponens (22), (21) | ¬¬∀f: ¬(b·Sf)=c | |||||||||
| (24) | Doppelte Negation (23) | ∀f: ¬(b·Sf)=c | |||||||||
| (25) | Konklusion (21), (24) | <¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> | |||||||||
| (26) | Hypothese | <¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> | |||||||||
| (27) | Abtrennung I (26) | ¬∀e: ¬(a·Se)=b | |||||||||
| (28) | Abtrennung II (26) | ¬∀f: ¬(b·Sf)=c | |||||||||
| (29) | Übernahme (25) | <¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> | |||||||||
| (30) | Modus ponens (29), (27) | ∀f: ¬(b·Sf)=c | |||||||||
| (31) | Hypothese | <¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> | |||||||||
| (32) | Übernahme (28) | ¬∀f: ¬(b·Sf)=c | |||||||||
| (33) | Konklusion (31), (32) | <<¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> ⇒ ¬∀f: ¬(b·Sf)=c> | |||||||||
| (34) | Kontraposition (33) | <¬¬∀f: ¬(b·Sf)=c ⇒ ¬<¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c>> | |||||||||
| (35) | Doppelte Negation (30) | ¬¬∀f: ¬(b·Sf)=c | |||||||||
| (36) | Modus ponens (34), (35) | ¬<¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> | |||||||||
| (37) | Konklusion (26), (36) | <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬<¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c>> | |||||||||
| (38) | Kontraposition (37) | <¬¬<¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> ⇒ ¬<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c>> | |||||||||
| (39) | Doppelte Negation (25) | ¬¬<¬∀e: ¬(a·Se)=b ⇒ ∀f: ¬(b·Sf)=c> | |||||||||
| (40) | Modus ponens (38), (39) | ¬<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> | |||||||||
| (41) | Konklusion (1), (40) | <∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c> ⇒ ¬<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c>> | |||||||||
| (42) | Kontraposition (41) | <¬¬<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c>> | |||||||||
| (43) | Hypothese | <¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> | |||||||||
| (44) | Doppelte Negation (43) | ¬¬<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> | |||||||||
| (45) | Übernahme (42) | <¬¬<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c>> | |||||||||
| (46) | Modus ponens (45), (44) | ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c> | |||||||||
| (47) | Konklusion (43), (46) | <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c>> | |||||||||