---

Step * of Lemma geo-perp-in_functionality

No Annotations
∀e:BasicGeometry. ∀x:Point.
  ∀[a,b,c,d:Point].
    ∀x':Point
      ∀[a',b',c',d':Point].
        (uiff(ab  ⊥x cd;a'b'  ⊥x' c'd')) supposing (d ≡ d' and c ≡ c' and b ≡ b' and a ≡ a' and x ≡ x')
BY
{ (Auto
   THEN (Assert ⌜Stable{a'b'  ⊥x' c'd'}⌝⋅ THEN EAuto 1)
   THEN Assert ⌜Stable{ab  ⊥x cd}⌝⋅
   THEN EAuto 1
   THEN RepeatFor 2 (Thin (-1))) }

1
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. ab  ⊥x cd
⊢ a'b'  ⊥x' c'd'

2
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}x:Point.
    \mforall{}[a,b,c,d:Point].
        \mforall{}x':Point
            \mforall{}[a',b',c',d':Point].
                (uiff(ab    \mbot{}x  cd;a'b'    \mbot{}x'  c'd'))  supposing 
                      (d  \mequiv{}  d'  and 
                      c  \mequiv{}  c'  and 
                      b  \mequiv{}  b'  and 
                      a  \mequiv{}  a'  and 
                      x  \mequiv{}  x')


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}Stable\{a'b'    \mbot{}x'  c'd'\}\mkleeneclose{}\mcdot{}  THEN  EAuto  1)
  THEN  Assert  \mkleeneopen{}Stable\{ab    \mbot{}x  cd\}\mkleeneclose{}\mcdot{}
  THEN  EAuto  1
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index