---

Step * 1 2 1 2 1 2 of Lemma geo-krippen-aux


1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c : Point
7. m1 : Point
8. m2 : Point
9. a1_c_a2
10. b1_c_b2
11. ca1 ≅ cb1
12. ca2 ≅ cb2
13. a1=m1=b1
14. a2=m2=b2
15. |ca1| ≤ |ca2|
16. a2 ≠ c
17. a : Point
18. a2=c=a
19. b : Point
20. b2=c=b
21. m2 ≠ c
22. m : Point
23. m2=c=m
24. a=m=b
25. |ca1| ≤ |ca|
26. c_a1_a
27. |cb1| ≤ |cb|
28. b2 ≠ c
29. c_b1_b
⊢ m1_c_m2
BY
{ ((InstLemma `not-not-double-pasch` [⌜e⌝;⌜a⌝;⌜a1⌝;⌜c⌝;⌜b⌝;⌜b1⌝;⌜m⌝]⋅ THENA Auto)
   THEN ((DoubleNegation THENA Auto) THENM (SupposeMore (-1) THENA Auto))
   THEN (RemoveDoubleNegation THENA Auto)
   THEN ExRepD) }

1
1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c : Point
7. m1 : Point
8. m2 : Point
9. a1_c_a2
10. b1_c_b2
11. ca1 ≅ cb1
12. ca2 ≅ cb2
13. a1=m1=b1
14. a2=m2=b2
15. |ca1| ≤ |ca2|
16. a2 ≠ c
17. a : Point
18. a2=c=a
19. b : Point
20. b2=c=b
21. m2 ≠ c
22. m : Point
23. m2=c=m
24. a=m=b
25. |ca1| ≤ |ca|
26. c_a1_a
27. |cb1| ≤ |cb|
28. b2 ≠ c
29. c_b1_b
30. q : Point
31. m_q_c
32. a1_q_b1
⊢ m1_c_m2

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c  :  Point
7.  m1  :  Point
8.  m2  :  Point
9.  a1\_c\_a2
10.  b1\_c\_b2
11.  ca1  \00D0  cb1
12.  ca2  \00D0  cb2
13.  a1=m1=b1
14.  a2=m2=b2
15.  |ca1|  \mleq{}  |ca2|
16.  a2  \mneq{}  c
17.  a  :  Point
18.  a2=c=a
19.  b  :  Point
20.  b2=c=b
21.  m2  \mneq{}  c
22.  m  :  Point
23.  m2=c=m
24.  a=m=b
25.  |ca1|  \mleq{}  |ca|
26.  c\_a1\_a
27.  |cb1|  \mleq{}  |cb|
28.  b2  \mneq{}  c
29.  c\_b1\_b
\mvdash{}  m1\_c\_m2


By

---

Latex:
((InstLemma  `not-not-double-pasch`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((DoubleNegation  THENA  Auto)  THENM  (SupposeMore  (-1)  THENA  Auto))
  THEN  (RemoveDoubleNegation  THENA  Auto)
  THEN  ExRepD)

---

Home Index