Step
*
of Lemma
eu-extend-property
∀e:EuclideanPlane
∀[q:Point]. ∀[a:{a:Point| ¬(q = a ∈ Point)} ]. ∀[b,c:Point]. (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)
BY
{ (Auto THEN D 1 THEN Unhide THEN D 2 THEN Auto) }
Latex:
Latex:
\mforall{}e:EuclideanPlane
\mforall{}[q:Point]. \mforall{}[a:\{a:Point| \mneg{}(q = a)\} ]. \mforall{}[b,c:Point].
(q\_a\_(extend qa by bc) \mwedge{} a(extend qa by bc)=bc)
By
Latex:
(Auto THEN D 1 THEN Unhide THEN D 2 THEN Auto)
Home
Index