---

Step * of Lemma plane-sep-imp-Opasch_left-strict

No Annotations
∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| B(abc)} . ∀x:Point. ∀y:{y:Point| b-x-y} .
  (x leftof ab ⇒ b # c ⇒ (∃p:Point [(a-x-p ∧ c-p-y)]))
BY
{ (Auto
   THEN ((FLemma `left-symmetry` [-2] THEN Auto) THEN FLemma `left-symmetry` [-1] THEN Auto)
   THEN (Assert B(abc) BY
               (DSetVars THEN Unhide THEN Auto))
   THEN (Assert b-x-y BY
               (DSetVars THEN Unhide THEN Auto))
   THEN (DVar `c' THEN Thin 5)
   THEN DVar `y'
   THEN Thin 7) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. x leftof ab
8. b # c
9. a leftof bx
10. b leftof xa
11. B(abc)
12. b-x-y
⊢ ∃p:Point [(a-x-p ∧ c-p-y)]

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  B(abc)\}  .  \mforall{}x:Point.  \mforall{}y:\{y:Point|  b-x-y\}  .
    (x  leftof  ab  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  (\mexists{}p:Point  [(a-x-p  \mwedge{}  c-p-y)]))


By

---

Latex:
(Auto
  THEN  ((FLemma  `left-symmetry`  [-2]  THEN  Auto)  THEN  FLemma  `left-symmetry`  [-1]  THEN  Auto)
  THEN  (Assert  B(abc)  BY
                          (DSetVars  THEN  Unhide  THEN  Auto))
  THEN  (Assert  b-x-y  BY
                          (DSetVars  THEN  Unhide  THEN  Auto))
  THEN  (DVar  `c'  THEN  Thin  5)
  THEN  DVar  `y'
  THEN  Thin  7)

---

Home Index