Step
*
1
of Lemma
geo-congruent-trivial
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. ¬aa ≅ bb
5. a # b
⊢ False
BY
{ (gProlong ⌜b⌝ ⌜a⌝ `xxx' ⌜b⌝ ⌜b⌝⋅ THEN EAuto 1) }
1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. ¬aa ≅ bb
5. a # b
6. xxx : Point
7. B(baxxx)
8. axxx ≅ bb
⊢ False
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. \mneg{}aa \mcong{} bb
5. a \# b
\mvdash{} False
By
Latex:
(gProlong \mkleeneopen{}b\mkleeneclose{} \mkleeneopen{}a\mkleeneclose{} `xxx' \mkleeneopen{}b\mkleeneclose{} \mkleeneopen{}b\mkleeneclose{}\mcdot{} THEN EAuto 1)
Home
Index