---

Step * of Lemma left-right-sep

∀g:OrientedPlane. ∀a,b,c,d:Point.  (a leftof cd ⇒ b leftof dc ⇒ a ≠ b)
BY
{ (Auto THEN (FLemma `use-plane-sep` [-1;-2] THENA Auto) THEN ExRepD THEN Assert ⌜a ≠ x⌝⋅ THEN Auto) }

1
.....assertion..... 
1. g : OrientedPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a leftof cd
7. b leftof dc
8. x : Point
9. Colinear(d;c;x)
10. b_x_a
⊢ a ≠ x

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}a,b,c,d:Point.    (a  leftof  cd  {}\mRightarrow{}  b  leftof  dc  {}\mRightarrow{}  a  \mneq{}  b)


By

---

Latex:
(Auto  THEN  (FLemma  `use-plane-sep`  [-1;-2]  THENA  Auto)  THEN  ExRepD  THEN  Assert  \mkleeneopen{}a  \mneq{}  x\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index