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. BasicGeometry
2. Point
3. P' Point
4. Point
5. 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