Step
*
of Lemma
geo-perp-in_wf
∀[e:BasicGeometry]. ∀[x,a,b,c,d:Point].  (ab  ⊥x cd ∈ ℙ)
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x,a,b,c,d:Point].    (ab    \mbot{}x  cd  \mmember{}  \mBbbP{})
By
Latex:
ProveWfLemma
Home
Index