Step
*
of Lemma
sq_stable__geo-perp-in
∀e:BasicGeometry. ∀x:Point.  ∀[a,b,c,d:Point].  SqStable(ab  ⊥x cd)
BY
{ (InstLemma `stable__geo-perp-in` [] THEN RepeatFor 6 (ParallelLast')) }
1
1. e : BasicGeometry
2. x : Point
3. [a] : Point
4. [b] : Point
5. [c] : Point
6. [d] : Point
7. Stable{ab  ⊥x cd}
⊢ SqStable(ab  ⊥x 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