# Morley Theorem -- using Wu's trick  
Let(A=[y2,y1], B=[u1,0], C=[u2,0], P=[0,1], Q=[y6,y5], R=[y4,y3]);
MorleyWu := Theorem(
     [arbitrary(A,B,C),equiangle(A,B,C,P,B,C,1,3),equiangle(A,C,B,P,C,B,1,3),
      tg([C,B,P],[P,C,B],[B,A,R])^2-3,equiangle(A,B,R,P,B,C),
      equiangle(A,C,Q,P,C,B),equiangle(B,A,R,Q,A,C)], 
     {equidistance(P,Q,P,R),equidistance(P,Q,Q,R)},[y1,y2,y3,y4,y5,y6]);

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.`,
`                                                                            `,
`For Wu's tricky formulation of the theorem, see`,
`W.-t. Wu: Basic Principles of Mechanical Theorem Proving in Elementary`, 
`Geometries. J. Syst. Sci. Math. Sci. 4 (1984) 207-235; J. Automat. Reason.`,
`2 (1986) 221-252.`
):
