Step
*
of Lemma
geo-gt_functionality
∀e:EuclideanPlane. ∀a1,a2,b1,b2,c1,c2,d1,d2:Point.
(a1 ≡ a2
⇒ b1 ≡ b2
⇒ c1 ≡ c2
⇒ d1 ≡ d2
⇒ (a1b1 > c1d1
⇐⇒ a2b2 > c2d2))
BY
{ (Intros THEN Unfold `geo-gt` 0 THEN RWO "-1 -2 -3 -4" 0 THEN Auto) }
Latex:
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a1,a2,b1,b2,c1,c2,d1,d2:Point.
(a1 \mequiv{} a2 {}\mRightarrow{} b1 \mequiv{} b2 {}\mRightarrow{} c1 \mequiv{} c2 {}\mRightarrow{} d1 \mequiv{} d2 {}\mRightarrow{} (a1b1 > c1d1 \mLeftarrow{}{}\mRightarrow{} a2b2 > c2d2))
By
Latex:
(Intros THEN Unfold `geo-gt` 0 THEN RWO "-1 -2 -3 -4" 0 THEN Auto)
Home
Index