---

Step * 2 of Lemma geo-congruent-symmetry


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab ≅ cd
7. ∀a:Point. (¬a # a)
8. ∀a,b,x,y:Point.  ((¬a # b) ⇒ B(xay) ⇒ B(xby))
9. ∀a,b,c:Point.  ((¬a # b) ⇒ ac ≅ cb)
10. ∀a,b,c,d:Point.  ((¬¬(∃w:Point. (B(cwd) ∧ cw ≅ ab))) ⇒ a # b ⇒ c # d)
11. ∀a,b,c:Point.  ((¬a # b) ⇒ B(abc))
12. ∀a,b,c:Point.  (B(abc) ⇒ B(cba))
13. ∀a,b,c,d:Point.  (B(abd) ⇒ B(bcd) ⇒ B(abc))
14. ∀a,b:Point.  aa ≅ bb
15. ∀a,b,p,q,r,s:Point.  (ab ≅ pq ⇒ ab ≅ rs ⇒ pq ≅ rs)
16. ∀a,b,c,d,A,B,C,D:Point.  (a # b ⇒ B(abc) ⇒ B(ABC) ⇒ ab ≅ AB ⇒ bc ≅ BC ⇒ ad ≅ AD ⇒ bd ≅ BD ⇒ cd ≅ CD)
17. ∀a,b,c,x,y:Point.  (ax ≅ ay ⇒ bx ≅ by ⇒ cx ≅ cy ⇒ x # y ⇒ (¬a # bc))
⊢ cd ≅ ab
BY
{ (InstHyp [⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜b⌝] (15)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  ab  \mcong{}  cd
7.  \mforall{}a:Point.  (\mneg{}a  \#  a)
8.  \mforall{}a,b,x,y:Point.    ((\mneg{}a  \#  b)  {}\mRightarrow{}  B(xay)  {}\mRightarrow{}  B(xby))
9.  \mforall{}a,b,c:Point.    ((\mneg{}a  \#  b)  {}\mRightarrow{}  ac  \mcong{}  cb)
10.  \mforall{}a,b,c,d:Point.    ((\mneg{}\mneg{}(\mexists{}w:Point.  (B(cwd)  \mwedge{}  cw  \mcong{}  ab)))  {}\mRightarrow{}  a  \#  b  {}\mRightarrow{}  c  \#  d)
11.  \mforall{}a,b,c:Point.    ((\mneg{}a  \#  b)  {}\mRightarrow{}  B(abc))
12.  \mforall{}a,b,c:Point.    (B(abc)  {}\mRightarrow{}  B(cba))
13.  \mforall{}a,b,c,d:Point.    (B(abd)  {}\mRightarrow{}  B(bcd)  {}\mRightarrow{}  B(abc))
14.  \mforall{}a,b:Point.    aa  \mcong{}  bb
15.  \mforall{}a,b,p,q,r,s:Point.    (ab  \mcong{}  pq  {}\mRightarrow{}  ab  \mcong{}  rs  {}\mRightarrow{}  pq  \mcong{}  rs)
16.  \mforall{}a,b,c,d,A,B,C,D:Point.
            (a  \#  b  {}\mRightarrow{}  B(abc)  {}\mRightarrow{}  B(ABC)  {}\mRightarrow{}  ab  \mcong{}  AB  {}\mRightarrow{}  bc  \mcong{}  BC  {}\mRightarrow{}  ad  \mcong{}  AD  {}\mRightarrow{}  bd  \mcong{}  BD  {}\mRightarrow{}  cd  \mcong{}  CD)
17.  \mforall{}a,b,c,x,y:Point.    (ax  \mcong{}  ay  {}\mRightarrow{}  bx  \mcong{}  by  {}\mRightarrow{}  cx  \mcong{}  cy  {}\mRightarrow{}  x  \#  y  {}\mRightarrow{}  (\mneg{}a  \#  bc))
\mvdash{}  cd  \mcong{}  ab


By

---

Latex:
(InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (15)\mcdot{}  THEN  Auto)

---

Home Index