Step * of Lemma Mid_perm

∀e:BasicGeometry. ∀A,B,C:Point.  (B=A=C ⇒ (B=A=C ∧ C=A=B))
BY
{ Auto }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. B=A=C
6. B=A=C
⊢ C=A=B


Latex:


Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,C:Point.    (B=A=C  {}\mRightarrow{}  (B=A=C  \mwedge{}  C=A=B))


By


Latex:
Auto




Home Index