---

Step * 1 of Lemma geo-congruent-functionality-lemma


1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
3. a1 : Point
4. a2 : Point
5. b1 : Point
6. b2 : Point
7. c1 : Point
8. c2 : Point
9. d1 : Point
10. d2 : Point
11. a1 ≡ a2
12. b1 ≡ b2
13. c1 ≡ c2
14. d1 ≡ d2
15. a1b1 ≅ c1d1
16. a1b1 ≅ a2b2
17. c1d1 ≅ c2d2
⊢ a2b2 ≅ c2d2
BY
{ ((FLemma `geo-congruent-transitivity` [-1;-3] THENA Auto)
   THEN (FLemma `geo-congruent-symmetry` [-3] THENA Auto)
   THEN FLemma `geo-congruent-transitivity` [-1;-2]
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  \mforall{}a,b,c:Point.    (a  \mequiv{}  b  {}\mRightarrow{}  ac  \mcong{}  bc)
3.  a1  :  Point
4.  a2  :  Point
5.  b1  :  Point
6.  b2  :  Point
7.  c1  :  Point
8.  c2  :  Point
9.  d1  :  Point
10.  d2  :  Point
11.  a1  \mequiv{}  a2
12.  b1  \mequiv{}  b2
13.  c1  \mequiv{}  c2
14.  d1  \mequiv{}  d2
15.  a1b1  \mcong{}  c1d1
16.  a1b1  \mcong{}  a2b2
17.  c1d1  \mcong{}  c2d2
\mvdash{}  a2b2  \mcong{}  c2d2


By

---

Latex:
((FLemma  `geo-congruent-transitivity`  [-1;-3]  THENA  Auto)
  THEN  (FLemma  `geo-congruent-symmetry`  [-3]  THENA  Auto)
  THEN  FLemma  `geo-congruent-transitivity`  [-1;-2]
  THEN  Auto)

---

Home Index