---

Step * 1 of Lemma geo-triangle_functionality

.....assertion..... 
1. e : HeytingGeometry
⊢ ∀a1,a2,b1,b2,c1,c2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ a1 # b1c1 ⇒ a2 # b2c2)
BY
{ (Assert ∀a,b,c,a2:Point.  (a ≡ a2 ⇒ a # bc ⇒ a2 # bc) BY
         (Auto THEN (FLemma `geo-triangle-implies` [-1] THENA Auto) THEN ExRepD THEN BHyp -1 THEN Auto)) }

1
1. e : HeytingGeometry
2. ∀a,b,c,a2:Point.  (a ≡ a2 ⇒ a # bc ⇒ a2 # bc)
⊢ ∀a1,a2,b1,b2,c1,c2:Point.  (a1 ≡ a2 ⇒ b1 ≡ b2 ⇒ c1 ≡ c2 ⇒ a1 # b1c1 ⇒ a2 # b2c2)

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  HeytingGeometry
\mvdash{}  \mforall{}a1,a2,b1,b2,c1,c2:Point.    (a1  \mequiv{}  a2  {}\mRightarrow{}  b1  \mequiv{}  b2  {}\mRightarrow{}  c1  \mequiv{}  c2  {}\mRightarrow{}  a1  \#  b1c1  {}\mRightarrow{}  a2  \#  b2c2)


By

---

Latex:
(Assert  \mforall{}a,b,c,a2:Point.    (a  \mequiv{}  a2  {}\mRightarrow{}  a  \#  bc  {}\mRightarrow{}  a2  \#  bc)  BY
              (Auto
                THEN  (FLemma  `geo-triangle-implies`  [-1]  THENA  Auto)
                THEN  ExRepD
                THEN  BHyp  -1
                THEN  Auto))

---

Home Index