---

Step * of Lemma geo-congruent-preserves-between

No Annotations
∀e:BasicGeometry. ∀[a,b,c,a',b',c':Point].  (B(a'b'c')) supposing (bc ≅ b'c' and ac ≅ a'c' and ab ≅ a'b' and B(abc))
BY
{ (Auto THEN (StableCases ⌜a' # a ∨ a' ≡ a⌝⋅ THENA Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. B(abc)
9. ab ≅ a'b'
10. ac ≅ a'c'
11. bc ≅ b'c'
12. a' # a ∨ a' ≡ a
⊢ B(a'b'c')

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. B(abc)
9. ab ≅ a'b'
10. ac ≅ a'c'
11. bc ≅ b'c'
12. ¬(a' # a ∨ a' ≡ a)
⊢ B(a'b'c')

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry
    \mforall{}[a,b,c,a',b',c':Point].    (B(a'b'c'))  supposing  (bc  \mcong{}  b'c'  and  ac  \mcong{}  a'c'  and  ab  \mcong{}  a'b'  and  B(abc))


By

---

Latex:
(Auto  THEN  (StableCases  \mkleeneopen{}a'  \#  a  \mvee{}  a'  \mequiv{}  a\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index