Step
*
of Lemma
geo-midpoint-diagonals-congruent2
∀e:BasicGeometry. ∀P,Q,R,S,P',Q',R',S',A:Point.  (((((P=A=P' ∧ Q=A=Q') ∧ R=A=R') ∧ S=A=S') ∧ PQ ≅ RS) 
⇒ P'Q' ≅ R'S')
BY
{ Auto }
1
1. e : BasicGeometry
2. P : Point
3. Q : Point
4. R : Point
5. S : Point
6. P' : Point
7. Q' : Point
8. R' : Point
9. S' : Point
10. A : Point
11. P=A=P'
12. Q=A=Q'
13. R=A=R'
14. S=A=S'
15. PQ ≅ RS
⊢ P'Q' ≅ R'S'
Latex:
Latex:
\mforall{}e:BasicGeometry.  \mforall{}P,Q,R,S,P',Q',R',S',A:Point.
    (((((P=A=P'  \mwedge{}  Q=A=Q')  \mwedge{}  R=A=R')  \mwedge{}  S=A=S')  \mwedge{}  PQ  \00D0  RS)  {}\mRightarrow{}  P'Q'  \00D0  R'S')
By
Latex:
Auto
Home
Index