Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 17 | ∀a: ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (2) | Spezialisierung (1) a ← (a·Se) | ∀b: ∀c: <(a·Se)=b ⇒ ((a·Se)·c)=(b·c)> | |||||||||
| (3) | Spezialisierung (2) b ← b | ∀c: <(a·Se)=b ⇒ ((a·Se)·c)=(b·c)> | |||||||||
| (4) | Spezialisierung (3) c ← Sf | <(a·Se)=b ⇒ ((a·Se)·Sf)=(b·Sf)> | |||||||||
| (5) | Theorem 21 | ∀a: ∀b: ∀c: (a·(b·c))=((a·b)·c) | |||||||||
| (6) | Spezialisierung (5) a ← a | ∀b: ∀c: (a·(b·c))=((a·b)·c) | |||||||||
| (7) | Spezialisierung (6) b ← Se | ∀c: (a·(Se·c))=((a·Se)·c) | |||||||||
| (8) | Spezialisierung (7) c ← Sf | (a·(Se·Sf))=((a·Se)·Sf) | |||||||||
| (9) | Hypothese | <(a·Se)=b∧(b·Sf)=c> | |||||||||
| (10) | Abtrennung I (9) | (a·Se)=b | |||||||||
| (11) | Übernahme (4) | <(a·Se)=b ⇒ ((a·Se)·Sf)=(b·Sf)> | |||||||||
| (12) | Modus ponens (11), (10) | ((a·Se)·Sf)=(b·Sf) | |||||||||
| (13) | Abtrennung II (9) | (b·Sf)=c | |||||||||
| (14) | Transitivität (12), (13) | ((a·Se)·Sf)=c | |||||||||
| (15) | Übernahme (8) | (a·(Se·Sf))=((a·Se)·Sf) | |||||||||
| (16) | Transitivität (15), (14) | (a·(Se·Sf))=c | |||||||||
| (17) | Konklusion (9), (16) | <<(a·Se)=b∧(b·Sf)=c> ⇒ (a·(Se·Sf))=c> | |||||||||
| (18) | Verallgemeinerung (17) nach f | ∀f: <<(a·Se)=b∧(b·Sf)=c> ⇒ (a·(Se·Sf))=c> | |||||||||
| (19) | Verallgemeinerung (18) nach e | ∀e: ∀f: <<(a·Se)=b∧(b·Sf)=c> ⇒ (a·(Se·Sf))=c> | |||||||||
| (20) | Theorem 43 | <∀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>> | |||||||||
| (21) | Modus ponens (20), (19) | <¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬(a·(Se·Sf))=c> | |||||||||
| (22) | Theorem 42 | <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c>> | |||||||||
| (23) | Theorem 44 | <¬∀e: ∀f: ¬(a·(Se·Sf))=c ⇒ ¬∀d: ¬(a·Sd)=c> | |||||||||
| (24) | Hypothese | <¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> | |||||||||
| (25) | Übernahme (22) | <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c>> | |||||||||
| (26) | Modus ponens (25), (24) | ¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c> | |||||||||
| (27) | Übernahme (21) | <¬∀e: ∀f: ¬<(a·Se)=b∧(b·Sf)=c> ⇒ ¬∀e: ∀f: ¬(a·(Se·Sf))=c> | |||||||||
| (28) | Modus ponens (27), (26) | ¬∀e: ∀f: ¬(a·(Se·Sf))=c | |||||||||
| (29) | Übernahme (23) | <¬∀e: ∀f: ¬(a·(Se·Sf))=c ⇒ ¬∀d: ¬(a·Sd)=c> | |||||||||
| (30) | Modus ponens (29), (28) | ¬∀d: ¬(a·Sd)=c | |||||||||
| (31) | Konklusion (24), (30) | <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀d: ¬(a·Sd)=c> | |||||||||
| (32) | Verallgemeinerung (31) nach c | ∀c: <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀d: ¬(a·Sd)=c> | |||||||||
| (33) | Verallgemeinerung (32) nach b | ∀b: ∀c: <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀d: ¬(a·Sd)=c> | |||||||||
| (34) | Verallgemeinerung (33) nach a | ∀a: ∀b: ∀c: <<¬∀e: ¬(a·Se)=b∧¬∀f: ¬(b·Sf)=c> ⇒ ¬∀d: ¬(a·Sd)=c> | |||||||||
Interpretation:
'teilt' ist transitiv