Questa pagina è stata trascritta, formattata e riletta. |
— 17 — |
- 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.
{P10 . §6 P11 : ⊃ P11}
- 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 . c = d : ⊃ : cd = ∧ : ⊃ Ts.(α)
Hp . d ∈ bc . §6 P3 . §7 P7 : ⊃ : cd ⊃ bc . bc ⊃ a′b : ⊃ Ts.(β)
Hp . c ∈ bd . (c, d) [d, c] (β) : ⊃ . Ts.(γ)
Hp . P1 . (α) (β) (γ) : ⊃ . Ts.}
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.
{Hp . P11 . §7 P4 . P3 : ⊃ : c′ca = ca ∪ a ∪ c′a = cb ∪ b ∪ ba ∪ a ∪ c′a = cb ∪ b ∪ c′cb : ⊃ Ts}
- 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.
{Hp . §7 P4 . §8 P11 . P3 : ⊃ : ab = ac ∪ c ∪ cb . c′ab = c′ac ∪ c′cb . c′ac = ca ∪ a ∪ c′a . c′cb = cb ∪ b ∪ c′b . c′a = b′a . c′b = a′b : ⊃ . Ts}
- a, b ∈ 1 . ⊃ . (ab)″ ⊃ b′a ∪ a ∪ ab ∪ b ∪ a′b.{P7 = P6}