Line Intersections

Textbook formulation:

Let O and U be two points in the plane of triangle ABC. Let AO, BO, CO intersect the opposite sides BC, CA, AB in P, Q, R. Let PU, QU, RU intersect QR, RP, PQ respectively in X,Y,Z. Show that AX, BY, CZ are concurrent.

Input to the system:

Proposition[\("Chou26", 
      any[A, B, C, O, U, P, Q, R, X, Y, Z, 
        II], 
triangle[A, B, 
          C] ∧ 
point[O, 
          U] ∧ 
inter[P, line[A, O], 
          line[B, C]] ∧ 
inter[Q, line[B, O], 
          line[C, A]] ∧ 
inter[R, line[C, O], 
          line[A, B]] ∧ 
inter[X, line[P, U], 
          line[Q, R]] ∧ 
inter[Y, line[Q, U], 
          line[R, P]] ∧ 
inter[Z, line[R, U], 
          line[P, Q]] ∧ 
inter[II, line[A, X], 
          line[B, Y]]

      \(\(\[Implies]\)\(collinear[II, C, Z]\)\)\)]

Input to the system:

KnowledgeBase["Chou26_g", 
      any[A, B, C, O, 
        U], 
{{A, {1, 
            3}}, {B, {-36, -62}}, {C, {-162, 143}}, {O, {151, 
            53}}, {U, {-144, 41}}}]

Input to the system:

Simplify[Proposition["Chou26"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Chou26_g"]]

Output generated automatically by the system

End of output

Input to the system:

KnowledgeBase["Chou26_g1", 
      any[A, B, C, O, 
        U], 
{{A, {10, 20}}, {B, {160, 300}}, {C, {400, 
            20}}, {O, {140, 100}}, {U, {180, 130}}}]

Input to the system:

Simplify[Proposition["Chou26"], by -> GraphicSimplifier, 
      using -> KnowledgeBase["Chou26_g1"]]

Output generated automatically by the system

End of output

Input to the system:

Prove[Proposition["Chou26"], by -> GeometryProver, 
      ProverOptions -> {Method -> "Wu", 
          Iterate -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook

Input to the system:

Prove[Proposition["Chou26"], by -> GeometryProver, 
      ProverOptions -> {Method -> "Wu"}]

Inserted notebook generated automatically by the system

End of inserted notebook

Input to the system:

Prove[Proposition["Chou26"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver"}]

Inserted notebook generated automatically by the system

End of inserted notebook

Prove[Proposition["Chou26"], by -> GeometryProver, 
      ProverOptions -> {Method -> "GroebnerProver", 
          MyAxis -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook

Input to the system:

Prove[Proposition["Chou26"], by -> GeometryProver, 
      ProverOptions -> {Method -> "Area", 
          OrtCoordSyst -> False}]

Inserted notebook generated automatically by the system

End of inserted notebook