Theorem([arbitrary(A,B,C), perpfoot(A,C,B,E,E), perpfoot(B,C,A,F,F), perpfoot(B,A,C,D,D), intersection(D,C,B,E,G)],[online(F,A,G)]) Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned Theorem: If the points A, B, and C are arbitrary, E is the perpendicular foot of the line AC to the line BE, F is the perpendicular foot of the line BC to the line AF, D is the perpendicular foot of the line BA to the line CD, and the two lines DC and BE intersect at G, then the point G is on the line FA. Proof: char set produced: [4 x1 1] [3 y1 1] [4 x2 1] [3 y2 1] [1 x3 1] [1 y3 1] [8 x4 1] [4 y4 1] pseudo-remainder: [4 y4 1] = u1*y4 + ... (3 terms) pseudo-remainder: [8 x4 1] = u1*y1*x4 + ... (7 terms) pseudo-remainder: [25 y3 1] = -u2^2*y3*y1*u1 + ... (24 terms) pseudo-remainder: [10 x3 1] = -v1*x3*u1*y1 + ... (9 terms) pseudo-remainder: [4 y2 1] = -u2*v1*y2*u1 + ... (3 terms) pseudo-remainder: [6 x2 1] = -x2*v1^2*u1*u2 + ... (5 terms) pseudo-remainder: [6 y1 1] = v1^3*u2^2*y1*u1 + ... (5 terms) pseudo-remainder: [4 x1 1] = u1^2*v1^2*x1 + ... (3 terms) `The theorem is true under the following subsidiary conditions:` . the line AC is non-isotropic . the line BA is non-isotropic . the line BC is non-isotropic . the line DC is not parallel to the line BE . the line AB is not perpendicular to the line BC . the line AC is not perpendicular to the line AB . the line AB is not perpendicular to the line BE QED.
