---

Step * of Lemma geo-extend_functionality

No Annotations
∀[e:BasicGeometry]. ∀[a:Point]. ∀[b:{b:Point| a # b} ]. ∀[c,d,a':Point]. ∀[b':{b':Point| a' # b'} ]. ∀[c',d':Point].
  (extend ab by cd ≡ extend a'b' by c'd') supposing (a ≡ a' and b ≡ b' and c ≡ c' and d ≡ d')
BY
{ (Auto THEN Assert ⌜extend ab by cd ≡ extend ab by c'd'⌝⋅) }

1
.....assertion..... 
1. e : BasicGeometry
2. a : Point
3. b : {b:Point| a # b} 
4. c : Point
5. d : Point
6. a' : Point
7. b' : {b':Point| a' # b'} 
8. c' : Point
9. d' : Point
10. d ≡ d'
11. c ≡ c'
12. b ≡ b'
13. a ≡ a'
⊢ extend ab by cd ≡ extend ab by c'd'

2
1. e : BasicGeometry
2. a : Point
3. b : {b:Point| a # b} 
4. c : Point
5. d : Point
6. a' : Point
7. b' : {b':Point| a' # b'} 
8. c' : Point
9. d' : Point
10. d ≡ d'
11. c ≡ c'
12. b ≡ b'
13. a ≡ a'
14. extend ab by cd ≡ extend ab by c'd'
⊢ extend ab by cd ≡ extend a'b' by c'd'

---

Latex:

---

Latex:
No  Annotations
\mforall{}[e:BasicGeometry].  \mforall{}[a:Point].  \mforall{}[b:\{b:Point|  a  \#  b\}  ].  \mforall{}[c,d,a':Point].  \mforall{}[b':\{b':Point|  a'  \#  b'\}  ].
\mforall{}[c',d':Point].
    (extend  ab  by  cd  \mequiv{}  extend  a'b'  by  c'd')  supposing  (a  \mequiv{}  a'  and  b  \mequiv{}  b'  and  c  \mequiv{}  c'  and  d  \mequiv{}  d')


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}extend  ab  by  cd  \mequiv{}  extend  ab  by  c'd'\mkleeneclose{}\mcdot{})

---

Home Index