Step * of Lemma sq_stable__geo-perp-in

e:BasicGeometry. ∀x:Point.  ∀[a,b,c,d:Point].  SqStable(ab  ⊥cd)
BY
(InstLemma `stable__geo-perp-in` [] THEN RepeatFor (ParallelLast')) }

1
1. BasicGeometry
2. Point
3. [a] Point
4. [b] Point
5. [c] Point
6. [d] Point
7. Stable{ab  ⊥cd}
⊢ SqStable(ab  ⊥cd)


Latex:


Latex:
\mforall{}e:BasicGeometry.  \mforall{}x:Point.    \mforall{}[a,b,c,d:Point].    SqStable(ab    \mbot{}x  cd)


By


Latex:
(InstLemma  `stable\_\_geo-perp-in`  []  THEN  RepeatFor  6  (ParallelLast'))




Home Index