---

Step * 2 of Lemma geo-perp-in_functionality


1. e : BasicGeometry
2. x : Point
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. x' : Point
8. a' : Point
9. b' : Point
10. c' : Point
11. d' : Point
12. x ≡ x'
13. a ≡ a'
14. b ≡ b'
15. c ≡ c'
16. d ≡ d'
17. a'b'  ⊥x' c'd'
⊢ ab  ⊥x cd
BY
{ (ParallelLast THEN RWO "-2 -3 -4 -5 -6 -7" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Point
3.  a  :  Point
4.  b  :  Point
5.  c  :  Point
6.  d  :  Point
7.  x'  :  Point
8.  a'  :  Point
9.  b'  :  Point
10.  c'  :  Point
11.  d'  :  Point
12.  x  \mequiv{}  x'
13.  a  \mequiv{}  a'
14.  b  \mequiv{}  b'
15.  c  \mequiv{}  c'
16.  d  \mequiv{}  d'
17.  a'b'    \mbot{}x'  c'd'
\mvdash{}  ab    \mbot{}x  cd


By

---

Latex:
(ParallelLast  THEN  RWO  "-2  -3  -4  -5  -6  -7"  0  THEN  Auto)

---

Home Index