Step * of Lemma eu-cong-angle-symm

e:EuclideanPlane. ∀a,b,c:Point.  abc cba supposing (a b ∈ Point)) ∧ (c b ∈ Point))
BY
Auto }

1
1. EuclideanPlane@i'
2. Point@i
3. Point@i
4. Point@i
5. ¬(a b ∈ Point)
6. ¬(c b ∈ Point)
⊢ abc cba


Latex:


Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    abc  =  cba  supposing  (\mneg{}(a  =  b))  \mwedge{}  (\mneg{}(c  =  b))


By


Latex:
Auto




Home Index