---

Step * 1 1 3 of Lemma geo-inner-three-segment


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ∀[d,A,B,C,D:Point].  (bd ≅ BD) supposing (cd ≅ CD and ad ≅ AD and bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
6. A : Point
7. B : Point
8. C : Point
9. ∀[D:Point]. (ba ≅ BD) supposing (ca ≅ CD and aa ≅ AD and bc ≅ BC and ac ≅ AC and B(ABC) and B(abc))
10. B(abc)
11. B(ABC)
12. ac ≅ AC
13. bc ≅ BC
14. ba ≅ BA
⊢ ab ≅ AB
BY
{ ((Assert ab ≅ ba BY
          Auto)
   THEN (FLemma `geo-congruent-transitivity` [-1;-2] THENA Auto)
   THEN (Assert BA ≅ AB BY
               Auto)
   THEN FLemma `geo-congruent-transitivity` [-1;-2]
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  \mforall{}[d,A,B,C,D:Point].
          (bd  \mcong{}  BD)  supposing  (cd  \mcong{}  CD  and  ad  \mcong{}  AD  and  bc  \mcong{}  BC  and  ac  \mcong{}  AC  and  B(ABC)  and  B(abc))
6.  A  :  Point
7.  B  :  Point
8.  C  :  Point
9.  \mforall{}[D:Point]
          (ba  \mcong{}  BD)  supposing  (ca  \mcong{}  CD  and  aa  \mcong{}  AD  and  bc  \mcong{}  BC  and  ac  \mcong{}  AC  and  B(ABC)  and  B(abc))
10.  B(abc)
11.  B(ABC)
12.  ac  \mcong{}  AC
13.  bc  \mcong{}  BC
14.  ba  \mcong{}  BA
\mvdash{}  ab  \mcong{}  AB


By

---

Latex:
((Assert  ab  \mcong{}  ba  BY
                Auto)
  THEN  (FLemma  `geo-congruent-transitivity`  [-1;-2]  THENA  Auto)
  THEN  (Assert  BA  \mcong{}  AB  BY
                          Auto)
  THEN  FLemma  `geo-congruent-transitivity`  [-1;-2]
  THEN  Auto)

---

Home Index