Step * 1 1 of Lemma plane-sep-imp-Opasch_left-strict


1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. leftof ab
8. c
9. leftof bx
10. leftof xa
11. B(abc)
12. b-x-y
13. leftof xa
14. leftof ax
15. Point
16. Colinear(a;x;d)
17. y-d-c
⊢ a-x-d
BY
((Assert BY
          ((Assert xd BY (((Assert bc BY EAuto 1) THEN (Assert xc BY EAuto 1)) THEN EAuto 1)) THEN Auto))
   THEN 0
   THEN Auto) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. Point
7. leftof ab
8. c
9. leftof bx
10. leftof xa
11. B(abc)
12. b-x-y
13. leftof xa
14. leftof ax
15. Point
16. Colinear(a;x;d)
17. y-d-c
18. d
⊢ B(axd)


Latex:


Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  x  leftof  ab
8.  b  \#  c
9.  a  leftof  bx
10.  b  leftof  xa
11.  B(abc)
12.  b-x-y
13.  c  leftof  xa
14.  y  leftof  ax
15.  d  :  Point
16.  Colinear(a;x;d)
17.  y-d-c
\mvdash{}  a-x-d


By


Latex:
((Assert  x  \#  d  BY
                ((Assert  y  \#  xd  BY
                                (((Assert  x  \#  bc  BY  EAuto  1)  THEN  (Assert  y  \#  xc  BY  EAuto  1))  THEN  EAuto  1))
                  THEN  Auto
                  ))
  THEN  D  0
  THEN  Auto)




Home Index