Step * 1 of Lemma straight-angle-sum1_symm


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. Point
11. Point
12. p' Point
13. d' Point
14. f' Point
15. abc ≅a ijp
16. kjp ≅a xyz
17. j_p'_p
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. x-y-z
22. b ≠ a ∧ b ≠ c
23. k-j-p
⊢ out(b ac)
BY
((InstLemma `angle-cong-preserves-zero-angle` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜i⌝;⌜j⌝;⌜p⌝]⋅ THEN EAuto 1)
   THEN InstLemma `geo-out_transitivity` [⌜e⌝;⌜j⌝;⌜p⌝;⌜d'⌝;⌜i⌝]⋅
   THEN EAuto 1) }

1
.....antecedent..... 
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. Point
9. Point
10. Point
11. Point
12. p' Point
13. d' Point
14. f' Point
15. abc ≅a ijp
16. kjp ≅a xyz
17. j_p'_p
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. x-y-z
22. b ≠ a
23. b ≠ c
24. k-j-p
⊢ out(j pd')


Latex:


Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  i  :  Point
9.  j  :  Point
10.  k  :  Point
11.  p  :  Point
12.  p'  :  Point
13.  d'  :  Point
14.  f'  :  Point
15.  abc  \mcong{}\msuba{}  ijp
16.  kjp  \mcong{}\msuba{}  xyz
17.  j\_p'\_p
18.  out(j  id')
19.  out(j  kf')
20.  d'-p'-f'
21.  x-y-z
22.  b  \mneq{}  a  \mwedge{}  b  \mneq{}  c
23.  k-j-p
\mvdash{}  out(b  ac)


By


Latex:
((InstLemma  `angle-cong-preserves-zero-angle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
  THEN  InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)




Home Index