# Morley Theorem
hyp := {x5**2*x2*x3-x3**2*x5*x8-x1**2*x8*x3+x3*x2*x1*x7*x6+x1*x5*x7*x3-x2*x1**2
*x7+x3**2*x5**2*x6+x3**2*x4**2*x6+x3**2*x4*x7-x4*x2*x1**2*x6+x1*x4*x8*x3+x3**2*
x1*x5-x1*x4**2*x3+x1**2*x4*x3-x1*x5**2*x3+x4**2*x2*x3+x5*x1**2*x2-x3**2*x1*x7-
x3*x1**2*x7*x6-x3*x1*x2*x4-x3*x5*x1*x2*x6-x4*x8*x3**2*x6+x3*x2*x1*x8+x5**2*x1*
x2*x6-x3*x7*x4*x2*x6-x1*x8*x5*x2-x1*x3*x5*x8*x6+x1*x7*x4*x2-x3*x2*x4*x8-x4*x1*
x3**2*x6-x5*x7*x3**2*x6+x2*x1**2*x8*x6-x1*x2*x4*x8*x6-x3*x2*x5*x7+x3*x1**2*x5*
x6-x1*x2*x5*x7*x6+x1*x3*x4*x7*x6+x1*x8*x3**2*x6+x4**2*x2*x1*x6+x3*x8*x5*x2*x6, 
-x5*x10*x2+x5*x2**2+x4*x9*x2-x2**2*x9-x5*x9*x3-x4*x10*x3+x4*x2*x3+x2*x10*x3-x2
**2*x3, x1*x8*x5*x2+x1*x7*x5*x9+x1*x7*x4*x2-x1*x7*x4**2-x4**2*x1*x9-x5**2*x7*x2
-x1*x5**2*x9-x5*x8*x4**2+x5*x4**2*x2-x4**2*x7*x10+x4*x7*x5**2-x5**2*x2*x9-x4**2
*x8*x9+x5**2*x8*x9-x1*x7*x5**2+x5**2*x7*x10-x4**2*x2*x9+x5**3*x2+x4**2*x5*x1-x4
**2*x7*x2-x4**2*x5*x10+x5**2*x4*x9+x4*x8*x2*x9+x5*x7*x2*x9+x1*x7*x4*x10-x1*x8*
x2*x9-x1*x8*x5*x10+x4*x1*x2*x9-2*x4*x7*x9*x5-x5*x8*x2*x10+x1*x8*x4*x9+2*x5*x8*
x10*x4-2*x4*x5*x2*x1+x4*x7*x2*x10+x1*x5*x2*x10+x4**3*x9-x5**3*x10-x1*x7*x2*x10+
x4**3*x7-x5**3*x8+x5**3*x1, -x5*x8*x1+x1**2*x5+x4*x7*x1-x1**2*x7-x5*x7*x3-x4*x8
*x3+x4*x1*x3+x1*x8*x3-x1**2*x3, x6**2-3, -x1**3*x5+3*x3**2*x1*x5-3*x1**2*x4*x3+
x4*x3**3+3*x1**3*x3-x1*x3**3, -x2**3*x5+3*x5*x3**2*x2-3*x4*x2**2*x3+x4*x3**3+3*
x2**3*x3-x2*x3**3}:
con :=
[x10*x3-x3*x8-x10*x7+x9*x8+x3*x9*x6-x7*x9*x6-x3*x7*x6+x6*x7**2-x8*x10*x6+x6*
x8**2,x8*x9-x8*x3-x7*x10+x3*x10+x7*x9*x6-x3*x9*x6-x3*x7*x6+x3**2*x6+x8*x10*x6]:
ord := [x4, x5, x6, x7, x8, x9, x10]:
Morley := Theorem(hyp,con,ord);

Remark(
`This is one of the most surprising theorems in elementary geometry discovered`,
`about 1899 by F. Morley (whose son Christopher wrote novels such as "Thunder`,
`on the Left").  He mentioned it to his friends, who spread it over the world`,
`in the  form  of  mathematical  gossip.  At  last,  after fifteen  years, an`,
`elementary  proof by  W. E. Philip  was published.  Many other proofs,  both`,
`elementary and trigonometrical, have appeared since then.`,
`  `,
`                                                        --- H. S. M. Coxeter`,
`                                      / Introduction to Geometry, pp. 23-24.`
):
