---

Step * of Lemma pgeo-join-plsep-sym

∀pg:ProjectivePlane. ∀a,b,c:Point. ∀s:a ≠ b. ∀s2:b ≠ a.  (c ≠ a ∨ b ⇒ c ≠ b ∨ a)
BY
{ ((Auto THEN (InstLemma `PL-sep-or` [⌜pg⌝;⌜c⌝;⌜a ∨ b⌝;⌜b ∨ a⌝]⋅ THENA Auto) THEN D -1 THEN Auto)
   THEN (InstLemma `pgeo-join-lsep-sym` [⌜pg⌝;⌜b⌝;⌜a⌝;⌜a ∨ b⌝;⌜s2⌝;⌜s⌝]⋅ THEN Auto)
   THEN RepeatFor 2 (D -1)
   THEN D -2
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  (InstLemma  `PL-sep-or`  [\mkleeneopen{}pg\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a  \mvee{}  b\mkleeneclose{};\mkleeneopen{}b  \mvee{}  a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1  THEN  Auto)
  THEN  (InstLemma  `pgeo-join-lsep-sym`  [\mkleeneopen{}pg\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a  \mvee{}  b\mkleeneclose{};\mkleeneopen{}s2\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  D  -2
  THEN  Auto)

---

Home Index