Step
*
2
of Lemma
stable_point-eq
1. e : EuclideanPlane
2. p : Point
3. q : Point
4. ¬¬(p = q ∈ Point)
5. pq=pp
⊢ p = q ∈ Point
BY
{ (FLemma `eu-congruence-identity` [-1] THEN Auto) }
Latex:
Latex:
1. e : EuclideanPlane
2. p : Point
3. q : Point
4. \mneg{}\mneg{}(p = q)
5. pq=pp
\mvdash{} p = q
By
Latex:
(FLemma `eu-congruence-identity` [-1] THEN Auto)
Home
Index