---

Step * of Lemma geo-opp-side_functionality

∀[e:BasicGeometry]. ∀[A,B,P,Q,A',B',P',Q':Point].  (A ≡ A' ⇒ B ≡ B' ⇒ P ≡ P' ⇒ Q ≡ Q' ⇒ (P-AB-Q ⇐⇒ P'-A'B'-Q'))
BY
{ (Auto THEN ParallelLast) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. A' : Point
7. B' : Point
8. P' : Point
9. Q' : Point
10. A ≡ A'
11. B ≡ B'
12. P ≡ P'
13. Q ≡ Q'
14. (¬(∀T:Point. (P_T_Q ⇒ (¬Colinear(A;B;T))))) ∧ (¬Colinear(A;B;P)) ∧ (¬Colinear(A;B;Q))
⊢ (¬(∀T:Point. (P'_T_Q' ⇒ (¬Colinear(A';B';T))))) ∧ (¬Colinear(A';B';P')) ∧ (¬Colinear(A';B';Q'))

2
1. e : BasicGeometry
2. A : Point
3. B : Point
4. P : Point
5. Q : Point
6. A' : Point
7. B' : Point
8. P' : Point
9. Q' : Point
10. A ≡ A'
11. B ≡ B'
12. P ≡ P'
13. Q ≡ Q'
14. (¬(∀T:Point. (P'_T_Q' ⇒ (¬Colinear(A';B';T))))) ∧ (¬Colinear(A';B';P')) ∧ (¬Colinear(A';B';Q'))
⊢ (¬(∀T:Point. (P_T_Q ⇒ (¬Colinear(A;B;T))))) ∧ (¬Colinear(A;B;P)) ∧ (¬Colinear(A;B;Q))

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[A,B,P,Q,A',B',P',Q':Point].
    (A  \mequiv{}  A'  {}\mRightarrow{}  B  \mequiv{}  B'  {}\mRightarrow{}  P  \mequiv{}  P'  {}\mRightarrow{}  Q  \mequiv{}  Q'  {}\mRightarrow{}  (P-AB-Q  \mLeftarrow{}{}\mRightarrow{}  P'-A'B'-Q'))


By

---

Latex:
(Auto  THEN  ParallelLast)

---

Home Index