---

Step * 3 of Lemma lsep-opposite-iff


1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ba
7. y leftof ab
8. x leftof ab ⇒ y leftof ba
9. x leftof ab ⇐ y leftof ba
⊢ ∃z:Point. (x_z_y ∧ Colinear(z;a;b))
BY
{ ((FLemma `use-plane-sep` [6;7] THENA Auto) THEN ParallelLast THEN D -1 THEN D 0 THEN Try (Trivial)) }

1
1. g : OrientedPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. x leftof ba
7. y leftof ab
8. x leftof ab ⇒ y leftof ba
9. x leftof ab ⇐ y leftof ba
10. x1 : Point
11. Colinear(b;a;x1)
12. x_x1_y
⊢ Colinear(x1;a;b)

---

Latex:

---

Latex:

1.  g  :  OrientedPlane
2.  a  :  Point
3.  b  :  Point
4.  x  :  Point
5.  y  :  Point
6.  x  leftof  ba
7.  y  leftof  ab
8.  x  leftof  ab  {}\mRightarrow{}  y  leftof  ba
9.  x  leftof  ab  \mLeftarrow{}{}  y  leftof  ba
\mvdash{}  \mexists{}z:Point.  (x\_z\_y  \mwedge{}  Colinear(z;a;b))


By

---

Latex:
((FLemma  `use-plane-sep`  [6;7]  THENA  Auto)  THEN  ParallelLast  THEN  D  -1  THEN  D  0  THEN  Try  (Trivial))

---

Home Index