---

Step * of Lemma pgeo-plsep-cycle

∀g:ProjectivePlane. ∀a,b,c:Point. ∀s:a ≠ b. ∀s1:b ≠ c. ∀s2:a ≠ c.  (a ≠ b ∨ c ⇒ {b ≠ a ∨ c ∧ c ≠ a ∨ b})
BY
{ ((Auto THEN (InstLemma `PL-sep-or` [⌜g⌝;⌜a⌝;⌜b ∨ c⌝;⌜a ∨ c⌝]⋅ THENA Auto) THEN Auto)
   THEN (InstLemma `psep-join-implies-false` [⌜g⌝]⋅ THEN Auto)
   THEN D -2) }

1
1. g : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : a ≠ b
6. s1 : b ≠ c
7. s2 : a ≠ c
8. a ≠ b ∨ c
9. a ≠ a ∨ c
10. ∀p,q:Point. ∀s:p ≠ q.  (p ≠ p ∨ q ⇒ False)
⊢ {b ≠ a ∨ c ∧ c ≠ a ∨ b}

2
1. g : ProjectivePlane
2. a : Point
3. b : Point
4. c : Point
5. s : a ≠ b
6. s1 : b ≠ c
7. s2 : a ≠ c
8. a ≠ b ∨ c
9. a ∨ c ≠ b ∨ c
10. ∀p,q:Point. ∀s:p ≠ q.  (p ≠ p ∨ q ⇒ False)
⊢ {b ≠ a ∨ c ∧ c ≠ a ∨ b}

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlane.  \mforall{}a,b,c:Point.  \mforall{}s:a  \mneq{}  b.  \mforall{}s1:b  \mneq{}  c.  \mforall{}s2:a  \mneq{}  c.
    (a  \mneq{}  b  \mvee{}  c  {}\mRightarrow{}  \{b  \mneq{}  a  \mvee{}  c  \mwedge{}  c  \mneq{}  a  \mvee{}  b\})


By

---

Latex:
((Auto  THEN  (InstLemma  `PL-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b  \mvee{}  c\mkleeneclose{};\mkleeneopen{}a  \mvee{}  c\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Auto)
  THEN  (InstLemma  `psep-join-implies-false`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  D  -2)

---

Home Index