---

Step * 1 2 1 of Lemma geo-left_functionality


1. e : EuclideanPlane
2. ∀a,b:Point.  (a # b ⇒ b # a)
3. ∀a1,a2,b,c:Point.  (a1 ≡ a2 ⇒ a1 leftof bc ⇒ a2 leftof bc)
4. a1 : Point
5. a2 : Point
6. b1 : Point
7. b2 : Point
8. c1 : Point
9. c2 : Point
10. a1 ≡ a2
11. b1 ≡ b2
12. c1 ≡ c2
13. a1 leftof b1c1
14. a2 leftof b1c1
⊢ a2 leftof b2c2
BY
{ (((FLemma `left-symmetry` [-1] THENA Auto) THEN (Assert b2 leftof c1a2 BY Auto))
   THEN (FLemma `left-symmetry` [-1] THENA Auto)
   THEN (Assert c2 leftof a2b2 BY
               Auto)
   THEN FLemma `left-symmetry` [-1]
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  \mforall{}a,b:Point.    (a  \#  b  {}\mRightarrow{}  b  \#  a)
3.  \mforall{}a1,a2,b,c:Point.    (a1  \mequiv{}  a2  {}\mRightarrow{}  a1  leftof  bc  {}\mRightarrow{}  a2  leftof  bc)
4.  a1  :  Point
5.  a2  :  Point
6.  b1  :  Point
7.  b2  :  Point
8.  c1  :  Point
9.  c2  :  Point
10.  a1  \mequiv{}  a2
11.  b1  \mequiv{}  b2
12.  c1  \mequiv{}  c2
13.  a1  leftof  b1c1
14.  a2  leftof  b1c1
\mvdash{}  a2  leftof  b2c2


By

---

Latex:
(((FLemma  `left-symmetry`  [-1]  THENA  Auto)  THEN  (Assert  b2  leftof  c1a2  BY  Auto))
  THEN  (FLemma  `left-symmetry`  [-1]  THENA  Auto)
  THEN  (Assert  c2  leftof  a2b2  BY
                          Auto)
  THEN  FLemma  `left-symmetry`  [-1]
  THEN  Auto)

---

Home Index