Principii di geometria/Principii di geometria
Questo testo è stato riletto e controllato. |
◄ | Notazioni | Note | ► |
PRINCIPII DI GEOMETRIA
§ 1. Punto e segmento.
Il segno =, fra due punti, indica la loro identità (coincidenza).
Se a, b sono punti, con ab intenderemo la classe formata dai punti interni al segmento ab. Quindi la formula c ∈ ab significa «c è un punto interno al segmento ab».
Assiomi sul segno =.
- a = a.
- a = b . = . b = a.
- a = b . b = c : ⊃ . a = c.
Assiomi sui segmenti.
- a, b ∈ 1 . ⊃ . ab ∈ K 1.
- a, b, c, d ∈ 1 . a = b . c = d : ⊃ . ac = bd.
§ 2. Definizioni.
- a, b ∈ 1 . ⊃ ∴ a′b = : 1 . [x ∈] (b ∈ ax).
- a, b ∈ 1 . ⊃ ∴ ab′ = : 1 . [x ∈] (a ∈ xb).
- a ∈ 1 . k ∈ K 1 : ⊃ ∴ ak = : 1 . [x ∈] (y ∈ k . x ∈ ay : − =y Λ).
- »: ⊃ ∴ a′k = : 1 . [x ∈] (y ∈ k . x ∈ a′y : − =y Λ).
- »: ⊃ ∴ ak′ = : 1 . [x ∈] (y ∈ k . x ∈ ay′ : − =y Λ).
- h, k ∈ K 1 : ⊃ ∴ hk = : 1 . [x ∈] (y ∈ h . x ∈ yk : − =y Λ).
- »: ⊃ ∴ h′k = : 1 . [x ∈] (y ∈ h . x ∈ y′k : − =y Λ).
- »: ⊃ ∴ hk′ = : 1 . [x ∈] (y ∈ h . x ∈ yk′ : − =y Λ).
- h ∈ K 1 . ⊃ . h″ = hh′.
- 2 = [x ∈] (a, b, c ∈ 1 . a − = b . x = (ab)″ : − =a, b Λ).
- a, b, c ∈ 1 . ⊃ ∷ a, b, c ∈ Cl . = ∴ r ∈ 2 . a, b, c ∈ r : − =r Λ.
- 3 = [x ∈] (a, b, c ∈ 1 . a, b, c − ∈ Cl . x = (abc)″ : − =a, b, c Λ).
- a, b, c, d ∈ 1 . ⊃ ∷ a, b, c, d ∈ Cp . = ∴ p ∈ 3 . a, b, c, d ∈ p : − =p ∧.
- Cnv . = . [x ∈] (x ∈ K 1 : a, b ∈ x . ⊃a, b . ab ⊃ x).
Abbreviazioni.
§ 3. Teoremi.
Sulle definizioni 1 e 2.
- a, b ∈ 1 . ⊃ ∴ c ∈ a′b . = : c ∈ 1 . b ∈ ac. {P1 = §2 P1}
- a, b, c ∈ 1 . ⊃ : c ∈ a′b . = . b ∈ ac.{P1 ⊃ P2}
- a, b, c ∈ 1 . ⊃ : c ∈ ab′ . = . a ∈ cb.{§2 P2 ⊃ P3}
- a, b, c ∈ 1 . ⊃ : a ∈ bc . = . b ∈ ac′ . = . c ∈ b′a.{P4 = : P2 . P3}
Sulle definizioni 3, 4, 5.
- a ∈ 1 . k ∈ K 1 : ⊃ ::: x ∈ ak . = ∷ x ∈ 1 ∴ y ∈ k . x ∈ ay : − =y ∧.
{P5 = §2 P3} - a ∈ 1 . k ∈ K 1 : ⊃ ∴ x ∈ ak . = : x ∈ 1 . k ∩ a′x − = ∧.{P6 = P5}
- »: ⊃ ∴ x ∈ a′k . = : x ∈ 1 . k ∩ ax − = ∧.{P7 = §2 P4}
- »: ⊃ ∴ x ∈ ak′ . = : x ∈ 1 . k ∩ x′a − = ∧.{P8 = §2 P5}
- a, b ∈ 1 . k ∈ K 1 : ⊃ : b ∈ ak . = . a ∈ bk′.{P6 . P8 : ⊃ P9}
- a ∈ 1 . h, k ∈ K 1 . h ⊃ k : ⊃ . ah ⊃ ak.
- » » : ⊃ . a′h ⊃ a′k.
- » » : ⊃ . ah′ ⊃ ak′.
- a ∈ 1 . h, k. ∈ K 1 : ⊃ . a (h ∪ k) = ah ∪ ak.
- »: ⊃ . a′ (h ∪ k) = a′h ∪ a′k.
- »: ⊃ . a (h ∪ k)′ = ah′ ∪ ak′.
- a ∈ 1 . k ∈ K 1 . k = ∧ : ⊃ : ak = ∧ . a′k = ∧ . ak′ = ∧.
Sulle definizioni 6, 7, 8.
- h, k ∈ K 1 : ⊃ ::: x ∈ hk . = ∷ x ∈ 1 ∴ y ∈ h . z ∈ k . x ∈ yz : − =y, z ∧.
- »::: x ∈ h′k . = » » x ∈ y′z »
- »::: x ∈ hk′ . = » » x ∈ yz′ »
- h, k, l ∈ K 1 . h ⊃ k : ⊃ hl ⊃ kl . h′l ⊃ k′l . hl′ ⊃ kl′.
- h, k, l ∈ K 1 : ⊃ : (h ∪ k)l = hl ∪ kl . (h ∪ k)′l = h′l ∪ k′l . (h ∪ k)l′ = hl′ ∪ kl′.
- h, k ∈ K 1 . h = ∧ : ⊃ . hk = h′k = hk′ = ∧.
Sulla definizione 9.
- k ∈ K 1 . ⊃ ∷ x ∈ k″ . = ∴ y, z ∈ k . x ∈ y′z : − =y, z ∧.
- h, k ∈ K 1 . h ⊃ k : ⊃ . h″ ⊃ k″.
- a ∈ 1 . k ∈ K 1 . b ∈ k : ⊃ . (ab)″ ⊃ (ak)″.
Sulle definizioni 10 e 12.
- x ∈ 2 . = ∴ a, b ∈ 1. a − = b . x ∈ (ab)″ : − =a, b ∧.
- a, b ∈ 1 . a − = b : ⊃ . (ab)″ ∈ 2.
- x ∈ 3 . = ∴ a, b, c ∈ 1 − Cl. x ∈ (abc)″ : − =a, b, c ∧.
- a, b, c ∈ 1 − Cl. ⊃ . (abc)″ ∈ 3.
Sulla definizione 14.
- h ∈ Cnv. = ∴ h K 1 : a, b ∈ h . ⊃a, b . ab ⊃ h.
- h, k ∈ Cnv. ⊃ . h ∩ k ∈ Cnv.
- k ∈ Cnv. l ∈ K 1 . l ⊃ k . a ∈ k : ⊃ . al ⊃ k.
- k ∈ Cnv. a, b, c ∈ k : ⊃ . abc ⊃ k.
- k ∈ Cnv. a, b, c, d ∈ k : ⊃ . abcd ⊃ k.
- k ∈ Cnv. a, b ∈ k : ⊃ . (ab)″ ⊃ k″.
§ 4. Assiomi I, II, III, IV.
Assioma I.
- 1 − = ∧.
Assioma II.
- a ∈ 1 . ⊃ ∴ x ∈ 1 . x − = a : − =x ∧.
Assioma III.
- a ∈ 1 . ⊃ . aa = ∧.
Teoremi.
- a, b ∈ 1 . a = b : ⊃ . ab = ∧.{Hp . ⊃ . ab = aa = ∧}
- a, b ∈ 1 . ab − = ∧ : ⊃ . a − = b.{P5 = P4}
- a, b ∈ 1 . c ∈ ab : ⊃ . a − = b.{Hp . ⊃ : ab − = ∧ . P5 : ⊃ Ts.}
- a, b, c ∈ 1 . b ∈ K 1 : ⊃ . a − ∈ a′k.{P7 = P6}
- a ∈ 1 . k ∈ K 1 : ⊃ . a − ∈ a′k.
Assioma IV.
- a, b ∈ 1 . a − = b : ⊃ . ab − = ∧.
Teoremi.
- a, b ∈ 1 . ab = ∧ : ⊃ . a = b.{P10 = P9}
- a, b ∈ 1 . ⊃ : a = b . = . ab = ∧.{P11 = : P4 . P10}
- a, b ∈ 1 . a − = b : ⊃ . b ∈ a′ab.
§5. Assiomi V, VI, VII.
Assioma V.
- a, b ∈ 1 . ⊃ . ab = ba.
Teoremi.
- a, b ∈ 1 . ⊃ . a′b = ba′.
- a, b ∈ 1 . k ∈ K 1 : ⊃ : b ∈ a′k . = . a ∈ b′k.{Hp . §3 P7 : ⊃ : b ∈ a′k . = . k ∩ ab − = ∧ . = . k ∩ ba − = ∧ . = a ∈ b′k : ⊃ . Ts.}
- a, b, c, d ∈ 1 . ⊃ : ab ∩ cd − = ∧ . = . a ∈ b′cd . = . b ∈ a′cd . = . c ∈ d′ab . = . d ∈ c′ab.
- ». ⊃ : a′b ∩ cd − = ∧ . = . a ∈ b(cd)′ . = . b ∈ acd . = . c ∈ d′a′b . = . d ∈ c′a′b.
- ». ⊃ : a′b ∩ c′d − = ∧ . = . a ∈ b(c′d′)′ . = . b ∈ ac′d . = . c ∈ d(a′b)′ . =. d ∈ ca′b.
- h, k ∈ K 1 . ⊃ . hk = kh.
- ». ⊃ . h′k = kh′.
Assioma VI.
- a, b ∈ 1 . ⊃ . a − ∈ ab.
Teoremi.
- a, b ∈ 1 . ⊃ . b − ∈ ab.{Hp . P9 . P1 : ⊃ : b − ∈ ba . ba = ab : ⊃ Ts}
- a, b ∈ 1 . c ∈ ab : ⊃ : c − = a . c − = b.{P11 = : P9 . P10}
- a, b ∈ 1 . c ∈ a′b : ⊃ : c − = . a . c − = b.{P12 = : P11 . §4 P7}
- a ∈ 1 . ⊃ . a′a = ∧.
- a ∈ 1 . ⊃ . a″ = ∧.
- a ∈ 1 . k ∈ K 1 : ⊃ . a − ∈ ak.
Assioma VII.
- a, b ∈ 1 . a − = b : ⊃ . a′b − = ∧.
Teoremi.
- a, b ∈ 1 . ⊃ : a′b = ∧ . = . a = b.{P17 = : P16 . P13}
- a, b ∈ 1 . a − = b : ⊃ . b ∈ aa′b.
§ 6. Assioma VIII.
- a, b, c, d ∈ 1 . c ∈ ad . b ∈ ac : ⊃ . b ∈ ad.
Teoremi.
- a, c, d ∈ 1 . c ∈ ad : ⊃ . ac ⊃ ad{P2 = P1}
- a, b ∈ 1 . c ∈ ab : ⊃ . ac ⊃ ab.{P3 = b [d] P2}
- » » : ⊃ . cb ⊃ ab.{P4 = (a, b) [b, a] P3}
- » » : ⊃ . ac ∪ c ∪ cb ⊃ ab.{P5 = : P3 . P4}
- a, b ∈ 1 . c ∈ ab . d ∈ ac : ⊃ . cd ⊃ ab.
- a, b ∈ 1 . c ∈ ab : ⊃ . c ∈ a′ab.{Hp . ⊃ : c − = a : ⊃ : ac − = ∧ . ac ⊃ ab . ⊃ : ac ∩ ab − = ∧ : ⊃ . Ts}
- a, b ∈ 1 . ⊃ . ab ⊃ a′ab.{P8 = P7}
- a, c ∈ 1 . b ∈ a′c : ⊃ . b ∈ a′ac.{P9 = P8}
- a, b ∈ 1 . ⊃ . a′b ⊃ a′ab.{P10 = P9}
- a, b ∈ 1 . a − = b : ⊃ . ab ∪ b ∪ a′b ⊃ a′ab.
- a, b, c ∈ 1 . b ∈ ac : ⊃ . a′c ⊃ a′b.{P12 = P1}
- a, c ∈ 1 . b ∈ ac : ⊃ . b ∈ aa′c.
- a, b ∈ 1 . ⊃ . ab ⊃ aa′b.{P14 = P13}
- a, b ∈ 1 . c ∈ a′b : ⊃ . c ∈ aa′b.{P15 = P13}
- a, b ∈ 1 . ⊃ . a′b ⊃ aa′b.{P16 = P15}
- a, b ∈ 1 . a − = b : ⊃ . ab ∪ b ∪ a′b ⊃ aa′b.
- a, b, c ∈ 1 . b ∈ ac . c ∈ ab : = ∧.
- a, b ∈ 1 . ⊃ . ab ∩ a′b = ∧.{P19 = P18}
- b, c ∈ 1 . ⊃ . c′b ∩ b′c = ∧.{P20 = P18}
- a, b ∈ 1 . ⊃ . a′b ∩ b′a = ∧.{P21 = P20}
- a, b, d ∈ 1 . a′b ∩ ad − = ∧ : ⊃ . b ∈ ad.{P22 = P1}
- a, b, d ∈ 1 . b ∈ aad : ⊃ . b ∈ ad.{P23 = P22}
- a, b ∈ 1 . ⊃ . aab ⊃ ab.{P24 = P23}
- a, b, d ∈ 1 . d ∈ a′a′b : ⊃ . d ∈ a′b.{P25 = P22}
- a, b ∈ 1 . ⊃ . a′a′b ⊃ a′b.{P26 = P25}
- a, b ∈ 1 . a − = b : ⊃ . b ∈ (ab)″.
- a, b ∈ 1 . ⊃ . ab ⊃ (ab)″.{Hp . x ∈ ab : ⊃ : x − = a . x ∈ (ax)″ . ax ⊃ ab . (ax)″ ⊃ (ab)″ : ⊃ . x ∈ (ab)″}
§ 7. Assioma IX.
- a, d ∈ 1 . b, c ∈ ad : ⊃ : b = c . ∪ . b ∈ ac . ∪ . b ∈ cd.
Teoremi.
- a, d ∈ 1 . c ∈ ad : ⊃ . ad ⊃ ac ∪ c ∪ cd.{P2 = P1}
- a, b ∈ 1 . c ∈ ab : ⊃ . ab ⊃ ac ∪ c ∪ cb.{P3 = P2}
- a, b ∈ 1 . c ∈ ab : ⊃ . ab = ac ∪ c ∪ cb.{P4 = : P3 . §6 P5}
- a, d ∈ 1 . b ∈ ad . c ∈ bd : ⊃ . b ∈ ac.{Hp . §6 P1 P18 : ⊃ : a, d ∈ 1 . b , c ∈ ad . b − = c . b − ∈ cd . P1 : ⊃ . Ts}
- a, d ∈ 1 . b ∈ ad : ⊃ . bd ⊃ a′b.{P6 = P5}
- a, b ∈ 1 . c ∈ a′b : ⊃ . bc ⊃ a′b.{P7 = (c) [d] P6}
- a, b ∈ 1 . c ∈ a′b : ⊃ . bc ∪ c ∪ a′c ⊃ a′b{P8 = : P7 . §6 P12}
- a, b ∈ 1 . c ∈ a′b : ⊃ . bc ∩ a′b − = ∧.
- a, b ∈ 1 . c ∈ a′b : ⊃ . c ∈ b′a′b.{P10 = P9}
- a, b ∈ 1 . ⊃ . a′b ⊃ b′a′b.{P11 = P10}
- a, c ∈ 1 . b ∈ ac : ⊃ . ac ∩ a′b − = ∧.
- a, c ∈ 1 . b ∈ ac : ⊃ . b ∈ aac.{P13 = P12}
- a, c ∈ 1 . ⊃ . ac ⊃ aac.{P14 = P13}
- a, b ∈ 1 . ⊃ . ab ⊃ aab{P15 = b [c] P14}
- a, b ∈ 1 . ⊃ aab = ab.{P16 = : P15 . §6 P24}
- a, b ∈ 1 . c ∈ a′b : ⊃ . c ∈ a′a′b.{P17 = P12}
- a, b ∈ 1 . ⊃ . a′b ⊃ a′a′b.{P18 = P17}
- a, b ∈ 1 . ⊃ . a′a′b = a′b.{P19 = : P18 . §6 P26}
- a ∈ 1 . k ∈ K 1 : ⊃ . aak = ak.
- » » : ⊃ . a′a′k = a′k.
- b, d ∈ 1 . c ∈ bd : ⊃ . d′b ⊃ c′b.{P22 = P5}
- a, b ∈ 1 . c ∈ a′b : ⊃ . a′c ⊃ b′c.{P23 = (a, b, c} [b, c, d] P22}
- a, b ∈ 1 . c ∈ a′b : ⊃ . b′c ∩ a′b − = ∧.
- a, b ∈ 1 . c ∈ a′b : ⊃ . c ∈ bba′.{P25 = 24}
- a, b ∈ 1 . ⊃ . a′b ⊃ bba′.{P26 = P25}
- a, b, c ∈ 1 . a′b ∩ b′c − = ∧ : ⊃ . b ∈ ac.{P27 = P5}
- a, b ∈ 1 . c ∈ bba′ : ⊃ . c ∈ ba′.{P28 = P27}
- a, b ∈ 1 . ⊃ . bba′ ⊃ ba′.{P29 = P28}
- a, b ∈ 1 . ⊃ . bba′ = ba′.{P30 = : P29 . P26}
- a ∈ 1 . k ∈ K 1 : ⊃ . aak′ = ak′.
- a, e ∈ 1 . c ∈ ae . b ∈ ac . d ∈ ce : ⊃ . c ∈ bd.
- a, e ∈ 1 . c ∈ ae . b ∈ ac . b ∈ ce : = ∧.
- a, e ∈ 1 . c ∈ ae : ⊃ . ac ∩ ce = ∧.{P34 = P33}
- a, b ∈ 1 . c ∈ ab : ⊃ . ac ∩ cb = ∧.{P35 = P34}
- a, b ∈ 1 . ⊃ . a′b ⊃ (ab)″.{Hp . x ∈ a′b : ⊃ ∴ c ∈ ab . d ∈ bc : − =c, d ∧ ∴ ⊃ ∴ c, d ∈ ab . x ∈ c′d : − =c, d ∧ ∴ ⊃ . x ∈ (ab)″}
- a , b ∈ 1 . a − = b : ⊃ . b′a ∪ a ∪ ab ∪ b ∪ a′b ⊃ (ab)″.
- a ∈ 1 . k ∈ K 1 . a − ∈ k : ⊃ . k′a ∪ a ∪ ak ∪ k ∪ a′k ⊃ (ak)″.
- a, b, c ∈ 1 . a − ∈ bc : ⊃ . (bc)′a ∪ a ∪ abc ∪ bc ∪ a′bc ⊃ (abc)″.
- a, b ∈ 1 . c ∈ a′b . d ∈ ac : ⊃ . d ∈ ab ∪ b ∪ a′b.
- a, b ∈ 1 . d ∈ aa′b : ⊃ . d ∈ ab ∪ b ∪ a′b.{P41 = P40}
- a, b ∈ 1 . ⊃ . aa′b ⊃ ab ∪ b ∪ a′b.{P42 = P41}
- a, b ∈ 1 . a − = b : ⊃ . aa′b = ab ∪ b ∪ a′b.
- a ∈ 1 . k ∈ K 1 . a − ∈ k : ⊃ . aa′k = ak ∪ k ∪ a′k.
- a, b ∈ 1 . c, d ∈ ab : ⊃ . cd ⊃ ab.
Hp . d ∈ ac . §6 P6 : ⊃ . Ts.(β)
Hp . d ∈ cb . (a, b) [b, a] (β) : ⊃ Ts.(γ)
Hp . P1 . (α) (β) (γ) : ⊃ . Ts.}
- a, b ∈ 1 . ⊃ . ab ∈ Cnv.{P46 = P45}
- a, b ∈ 1 . ⊃ . a ∪ ab ∈ Cnv.
- ». ⊃ . a ∪ ab ∪ b ∈ Cnv.
§ 8. Assioma X.
- a, b ∈ 1 . c, d ∈ a′b : ⊃ : c = d . ∪ . d ∈ bc . ∪ . c ∈ bd.
Teoremi.
- a, b ∈ 1 . c ∈ a′b : ⊃ . a′b ⊃ bc ∪ c ∪ b′c.{P2 = P1}
- a, b ∈ 1 . c ∈ a′b : ⊃ . a′b ⊃ bc ∪ c ∪ a′c.{P2 . §7 P23 : ⊃ P3}
- a, b ∈ 1 . c ∈ a′b : ⊃ . a′b = bc ∪ c ∪ a′c.{P4 = : P3 . §7 P8}
- a, b ∈ 1 . c ∈ a′b : ⊃ . a′b ⊃ ac ∪ c ∪ a′c.
- a, b ∈ 1 . c, d ∈ a′b : ⊃ . d ∈ ac ∪ c ∪ a′c.{P6 = P5}
- a, c, d ∈ 1 . ac ∩ ad − = ∧ : ⊃ . d ∈ ac ∪ c ∪ a′c.{P7 = P6}
- a, c ∈ 1 . d ∈ a′ac : ⊃ . d ∈ ac ∪ c ∪ a′c.{P8 = P7}
- a, c ∈ 1 . ⊃ . a′ac ⊃ ac ∪ c ∪ a′c.{P9 = P8}
- a, b ∈ 1 . ⊃ . a′ab ⊃ ab ∪ b ∪ a′b.{P10 = P9}
- a, b ∈ 1 . a − = b : ⊃ . a′ab = ab ∪ b ∪ a′b.
- a, b ∈ 1 : ⊃ . a′ab = aa′b.{P11 . §7 P43 : ⊃ P12}
- a ∈ 1 . k ∈ K 1 : ⊃ . a′ak = aa′k.
- a, b ∈ 1 . c, d ∈ a′b : ⊃ . cd ⊃ a′b.
Hp . d ∈ bc . §6 P3 . §7 P7 : ⊃ : cd ⊃ bc . bc ⊃ a′b : ⊃ Ts.(β)
Hp . c ∈ bd . (c, d) [d, c] (β) : ⊃ . Ts.(γ)
Hp . P1 . (α) (β) (γ) : ⊃ . Ts.}
- a, b ∈ 1 . ⊃ . a′b ∈ Cnv.{P15 = P14}
- a, b ∈ 1 . ⊃ . b ∪ a′b ⊃ Cnv.{P16 = : P15 . §7 P7}
- a, b, c ∈ 1 . b ∈ ca : ⊃ . c′ca = c′cb.
- a, b, c ∈ 1 . b ∈ c′a : ⊃ . c′ca = c′cb.{P18 = (b, a) [a, b] P17}
- a, c ∈ 1 . b ∈ c′ca : ⊃ . c′ca = c′cb.{P19 = : P17 . P18}
§ 9. Assioma XI.
- a, b, c, d ∈ 1 . b ∈ ac . c ∈ bd : ⊃ . c ∈ ad.
Teoremi.
- a, b, c ∈ 1 . b ∈ ac : ⊃ . b′c ⊃ a′c.{P2 = P1}
- a, b, c ∈ 1 . b ∈ ac : ⊃ . b′c = a′c.{P3 = : P2 . §7 P23}
- a, b, c ∈ 1 . b ∈ c′a : ⊃ . b′c = a′c.{P4 = (b, a) [a, b] P3}
- a, c ∈ 1 . b ∈ c′ca : ⊃ . b′c = a′c.{P3 . P4 . §8 P11 : ⊃ . P5}
- a, b ∈ 1 . c ∈ ab : ⊃ . c′ab ⊃ b′a ∪ a ∪ ab ∪ b ∪ a′b.
- a, b ∈ 1 . ⊃ . (ab)″ ⊃ b′a ∪ a ∪ ab ∪ b ∪ a′b.{P7 = P6}
- a, b ∈ 1 . a − = b : ⊃ . (ab)″ = b′a ∪ a ∪ ab ∪ b ∪ a′b.
- a, b ∈ 1 . a − = b : ⊃ . (ab)″ = b′ba ∪ b ∪ a′b.
- a, c ∈ 1 . b ∈ c′ca : ⊃ . (ac)″ = (bc)″.{P9 . P5 . §8 P19 : ⊃ P10}
- a, c ∈ 1 . b ∈ a′c : ⊃ . b′c = c′ca.
- a, c ∈ 1 . b ∈ a′c : ⊃ . (ac)″ = (bc)″.
- a, c ∈ 1 . b ∈ (ac)″ . b − = c : ⊃ . (ac)″ = (bc)″.
- a, b ∈ 1 . c, d ∈ (ab)″ . c − = d : ⊃ . (ab)″ = (cd)″.(P13 ⊃ P14}
- r ∈ 2 . c, d ∈ r . c − = d : ⊃ . r = (cd)″.{P15 = P14}
- r, s ∈ 2 . a, b ∈ 1 . a, b ∈ r ∩ s . a − = b : ⊃ . r = s.
- a, b ∈ 1 . ⊃ . (ab)″ Cnv.{P14 ⊃ P17}
- 2 ⊃ Cnv.
- a, b, c ∈ 1 . a − = b : ⊃ : a, b, c ∈ Cl . = . c ∈ (ab)″.
- a, b, c ∈ 1 . ⊃ ∴ a, b, c ∈ Cl : = : a = b . ∪ . a = c . ∪ . b = c . ∪ . a ∈ bc . ∪ . b ∈ ac . ∪ . c ∈ ab.
- a, b, c ∈ 1 . d ∈ bc : ⊃ : a, b, c ∈ Cl . = . a, b, d, ∈ Cl.
- a, b, c ∈ 1 . e ∈ abc : ⊃ : a, b, c ∈ Cl . = . a, b, e ∈ Cl.
§ 10. Assiomi XII e XIII.
Assioma XII.
- r ∈ 2 . ⊃ ∴ x ∈ 1 . x − ∈ r : − =x ∧.
Assioma XIII.
- a, b, c ∈ 1 . a, b, c − ∈ Cl . d ∈ bc . e ∈ ad : ⊃ ∴ f ∈ ac . e ∈ bf : − =f ∧.
Teoremi.
- a, b, c, e ∈ 1 . a, b, c − ∈ Cl . bc ∩ a′e − = ∧ : ⊃ . ac ∩ b′e − = ∧.
- a, b, c, e ∈ 1 . a, b, c − ∈ Cl : ⊃ : bc ∩ a′e − = ∧ . = . ac ∩ b′e − = ∧.
- a, b, c ∈ 1 − Cl . ⊃ : e ∈ abc . = . e ∈ bac.{P5 = P4}
- a, b, c ∈ 1 − Cl . ⊃ . abc = bac.{P6 = P5}
- ». ⊃ . abc = (ab)c.
- a, b, e ∈ 1 − Cl . ⊃ : c ∈ b′a′e . = . c ∈ a′b′e . = . c ∈ (ab)′e.
- a, b, c ∈ 1 − Cl . ⊃ . b′a′c = a′b′c = (ab)′c.{P9 = P8}
- a, b, c ∈ 1 − Cl . p ∈ ab . q ∈ ac : ⊃ . pq ⊃ abc.
- a, b, c ∈ 1 . a − ∈ bc . p ∈ ab . q ∈ ac : ⊃ . pq ⊃ abc.
- k ∈ Cnv . a ∈ 1 . a − ∈ k . b, c ∈ k . p ∈ ab . q ∈ ac : ⊃ . pq ⊃ ak.
- k ∈ Cnv . a ∈ 1 . a − ∈ k : ⊃ . ak Cnv.{P13 = P12}
- a, b, c ∈ 1 . a − ∈ bc : ⊃ . abc ∈ Cnv.
- a, b, c, d ∈ 1 . b − ∈ cd . a − ∈ bcd : ⊃ . abcd ∈ Cnv.
- k ∈ Cnv . a ∈ 1 . a − ∈ k : ⊃ . ak ∪ k ∈ Cnv.
- k ∈ Cnv . a ∈ 1 : ⊃ . a ∪ ak ∈ Cnv.
- k ∈ Cnv . a ∈ 1 : ⊃ . a ∪ ak ∪ k ∈ Cnv.
- a, b, c ∈ 1 − Cl . d ∈ bc . e ∈ ad . x ∈ b′e : ⊃ . x ∈ adc ∪ ac ∪ b′ac.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . b′ad ⊃ adc ∪ ac ∪ b′ac.{P20 = P19}
- a, b, c ∈ 1 − Cl . ⊃ . bc′ ⊃ (abc)″.
- a, b, c ∈ 1 − Cl . ⊃ . a ∪ b ∪ c ∪ ab ∪ ... ∪ a′b ∪ ... ∪ abc ∪ a′bc ∪ ... ∪ a′b′c ∪ ... ⊃ (abc)″.{P21 . §7 P39 : ⊃ P22}
- a, b, c ∈ 1 − Cl . ⊃ . (bc)″ ⊃ (abc)″.
- a, b, c ∈ 1 − Cl . r = (bc)″ : ⊃ . a′r ⊃ (abc)″.
- p ∈ 3 . r ∈ 2 : ⊃ ∴ x ∈ p . x − ∈ r : − =x ∧.
- a, b, c ∈ 1 − Cl . p ∈ abc : ⊃ . abc = p ∪ pa ∪ pab ∪ pb ∪ pbc ∪ pc ∪ pca.
- a, b, c ∈ 1 − Cl . p, q ∈ abc . p − = q : ⊃ . p′q ∩ (a ∪ ab ∪ b ∪ bc ∪ c ∪ ca) − = ∧.
- r ∈ 2 . a ∈ 1 . a − ∈ r . b ∈ r . c ∈ b′a . d ∈ a′r : ⊃ . d ∈ c′r.
- r ∈ 2 . a ∈ 1 . a − ∈ r . b ∈ r . c ∈ b′a : ⊃ . a′r ⊃ c′r.{P29 = P28}
- r ∈ 2 . c ∈ 1 . c − ∈ r . a ∈ cr : ⊃ . a′r ⊃ c′r.{P30 = P29}
- a, b, c ∈ 1 . − Cl . p ∈ abc : ⊃ . p′abc ⊃ a ∪ ... ∪ ab ∪ ... ∪ a′b ∪ ... ∪ abc ∪ a′bc ∪ ... ∪ a′b′c ∪ ...
- a, b, c ∈ 1 − Cl : ⊃ . (abc)″ = a ∪ b ∪ c ∪ ab ∪ ac ∪ bc ∪ a′b ∪ ab′ ∪ b′c ∪ cb′ ∪ c′a ∪ ac′ ∪ abc ∪ a′bc ∪ b′ca ∪ c′ab ∪ a′b′c ∪ b′c′a ∪ c′a′b.{P22 . P31 : ⊃ . P32}
- a, b, c ∈ 1 − Cl . ⊃ ∴ x ∈ (abc)″ : = : a, b, x ∈ Cl . ∪ . a, c, x ∈ Cl . ∪ . b, c, x ∈ Cl . ∪ . x ∈ abc . ∪ . a ∈ bcx . ∪ . b ∈ acx . ∪ . c ∈ abx . ∪ . ax ∩ bc − = ∧ . ∪ . bx ∩ ac − = ∧ . ∪ . cx ∩ ab − = ∧.
§ 11. Assioma XIV.
- a, b, c ∈ 1 . a, b, c − ∈ Cl . d ∈ bc . f ∈ ac : ⊃ ∴ e ∈ ad . e ∈ bf : − =e ∧.
Teoremi.
- a, b, d, f ∈ 1 . a, b, d − ∈ Cl . b′d ∩ a′f − = ∧ : ⊃ . ad ∩ bf − = ∧.
- a, b, d ∈ 1 − Cl . f ∈ a′bd : ⊃ . f ∈ b′ad.{P3 = P2}
- a, b, c ∈ 1 − Cl . ⊃ . ab′c ⊃ b′ac.
- a, b, c ∈ 1 − Cl . p ∈ a′b . q ∈ a′c : ⊃ . pq ⊃ a′bc.
- h ∈ Cnv . a ∈ 1 . a − ∈ h : ⊃ a′h ∈ Cnv.
- h ∈ Cnv . a ∈ 1 . a − ∈ h : ⊃ . ah ∪ h ∪ a′h ∈ Cnv.
- h ∈ Cnv . a ∈ 1 . a − ∈ h : ⊃ . h ∪ a′h ∈ Cnv.
- a, b, c ∈ 1 − Cl . p ∈ b′a . q ∈ c′a : ⊃ . pq ⊃ b′c′a.
- h ∈ Cnv . a ∈ 1 . a − ∈ h : ⊃ . h′a ∈ Cnv.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . adc ⊃ b′ad.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . ac ⊃ b′ad.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . b′ac ⊃ b′ad.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . adc ∪ ac ∪ b′ac ⊃ b′ad.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . b′ad = adc ∪ ac ∪ b′ac.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . d′ab = c′ab ∪ c′a ∪ c′d′a.
- a, b, c ∈ 1 − Cl . d ∈ bc : ⊃ . (abc)″ = (abd)″.
- a, b, c ∈ 1 − Cl . d ∈ (bc)″ . d − = b : ⊃ . (abc)″ = (abd)″.
- a, b, c ∈ 1 − Cl . d ∈ abc : ⊃ . (abc)″ = (abd)″.
- a, b, c ∈ 1 − Cl . d ∈ a′bc : ⊃ . (abc)″ = (abd)″.
- a, b, c ∈ 1 − Cl . d ∈ (abc)″ . d − ∈ (ab)″ : ⊃ . (abc)″ = (abd)″.
- a, b, c ∈ 1 − Cl . d, e ∈ (abc)″ . a, d, e − ∈ Cl : ⊃ . (abc)″ = (ade)″.
- a, b, c ∈ 1 − Cl . d, e, f ∈ (abc)″ . d, e, f − ∈ Cl : ⊃ . (abc)″ = (def)″.
- p ∈ 3 . a, b, c ∈ p . a, b, c − ∈ Cl : ⊃ . p = (abc)″.
- p, q ∈ 3 . a, b, c ∈ p ∩ q . a, b, c − ∈ Cl : ⊃ . p = q.
- 3 ⊃ Cnv.
- a, b, c, d ∈ 1 . a, b, c − ∈ Cl : ⊃ . a, b, c, d ∈ Cp . = . d ∈ (abc)″.
- a, b, c, d ∈ 1 . ⊃ ∴ a, b, c, d ∈ Cp . = : a, b, c ∈ Cl . ∪ . a, b, d ∈ Cl . ∪ . a, c, d ∈ Cl . ∪ . b, c, d ∈ Cl . ∪ . a ∈ bcd . ∪ . b ∈ acd . ∪ . c ∈ abd . ∪ . d ∈ abc . ∪ . ab ∩ cd − = ∧ . ∪ . ac ∩ bd − = ∧ . ∪ . ad ∩ bc − = ∧.
- p ∈ 3 . r ∈ 2 . a, b ∈ p ∩ r . a − = b : ⊃ . r ⊃ p.
- r ∈ 2 . a ∈ 1 . a − ∈ r . c ∈ b′a . d ∈ c′r : ⊃ . d ∈ a′r.
- r ∈ 2 . c ∈ 1 . c − ∈ r . a ∈ cr : ⊃ . c′r ⊃ a′r{P31 = P30}
- r ∈ 2 . c ∈ 1 . c − ∈ r . a ∈ cr : ⊃ . a′r = c′r.
- r ∈ 2 . a ∈ 1 . a − ∈ r . b ∈ r′ra : ⊃ . a′r = b′r.
- r ∈ 2 . a ∈ 1 . a − ∈ r . c ∈ a′r . b ∈ c′r : ⊃ . b ∈ r′ra.
- r ∈ 2 . a ∈ 1 . a − ∈ r . b ∈ r′ra : ⊃ . r′ra = r′rb.
- r ∈ 2 . a ∈ 1 . a − ∈ r : ⊃ . (ar)″ ∈ 3.
- »»: ⊃ . (ar)″ = r ∪ ra′ ∪ r′ra.
- p ∈ 3 . a ∈ 1 . a − ∈ p . b ∈ p′pa : ⊃ . a′p = b′p.
- »». c ∈ a′p . b ∈ c′p : ⊃ . b ∈ p′pa.
- »». b ∈ p′pa : ⊃ . p′pa = p′pb.
§ 12. Assiomi XV e XVI.
Assioma XV.
- p ∈ 3 . ⊃ ∴ a ∈ 1 . a − ∈ p : − =a ∧.
Assioma XVI.
- p ∈ 3 . a ∈ 1 . a − ∈ p . b ∈ a′p . x ∈ 1 : ⊃ : x ∈ p . ∪ . ax ∩ p − = ∧ . ∪ . bx ∩ p − = ∧.
Teoremi.
- p ∈ 3 . a ∈ 1 . a − ∈ p . b ∈ a′p . c ∈ 1 : ⊃ . p ∩ (ac ∪ c ∪ cb) − = ∧.
- p, q ∈ 3 . a ∈ p ∩ q : ⊃ ∴ r ∈ 2 . r ⊃ p ∩ q : − =r ∧.