Step * of Lemma eu-between_wf

[e:EuclideanStructure]. ∀[a,b,c:Point].  (a-b-c ∈ ℙ)
BY
(ProveWfLemma THEN All (Unfold `eu-point`)⋅ THEN DRecord THEN Auto) }


Latex:


Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b,c:Point].    (a-b-c  \mmember{}  \mBbbP{})


By


Latex:
(ProveWfLemma  THEN  All  (Unfold  `eu-point`)\mcdot{}  THEN  DRecord  1  THEN  Auto)




Home Index