Step
*
of Lemma
at-most-one-midpoint
∀e:BasicGeometry. ∀P,P',A,B:Point.  ((P=A=P' ∧ P=B=P') 
⇒ A ≡ B)
BY
{ ((Auto THEN gSeparatedCases ⌜A⌝⌜B⌝⋅) THENA Auto) }
1
1. e : BasicGeometry
2. P : Point
3. P' : Point
4. A : Point
5. B : Point
6. P=A=P'
7. P=B=P'
8. A ≠ B
⊢ A ≡ B
Latex:
Latex:
\mforall{}e:BasicGeometry.  \mforall{}P,P',A,B:Point.    ((P=A=P'  \mwedge{}  P=B=P')  {}\mRightarrow{}  A  \mequiv{}  B)
By
Latex:
((Auto  THEN  gSeparatedCases  \mkleeneopen{}A\mkleeneclose{}\mkleeneopen{}B\mkleeneclose{}\mcdot{})  THENA  Auto)
Home
Index