Theorems

1. Theorem([arbitrary(C,A), midpoint(A,C,F), intersection(A,E,B,F,G), midpoint(A,B,D), midpoint(C,B,E)],[online(D,C,G)])
   Warning: the coordinates of the points from {A, B, C, D, E, F, G} are reassigned
   
   
   Theorem: If the points C and A are arbitrary, F is the midpoint of A and C, the two lines AE and BF intersect at G, D is the midpoint of A and B, and E is the midpoint of C and B, then the point G is on the line DC.
   
   Proof:
   
   char set produced: [2 x1 1] [1 y1 1] [2 x3 1] [2 y3 1] [12 x4 1] [4 y4 1] [3 x5 1] [2 y5 1]
   pseudo-remainder: [2 y5 1] = y5*x4 + ... (1 terms)
   pseudo-remainder: [2 x5 1] = -2*x5*y4 + ... (1 terms)
   pseudo-remainder: [3 y4 1] = -u1*y4 + ... (2 terms)
   pseudo-remainder: [6 x4 1] = -y2*x4*u1 + ... (5 terms)
   pseudo-remainder: [14 y3 2] = -u1^2*x1*y3^2 + ... (13 terms)
   pseudo-remainder: [8 x3 2] = y1*x3^2*y2 + ... (7 terms)
   pseudo-remainder: [4 y1 1] = -u1^2*y1*y2 + ... (3 terms)
   pseudo-remainder: [2 x1 1] = -4*y2^2*u1*x1 + ... (1 terms)
   
   `The theorem is true under the following subsidiary conditions:`
   . the line AE is not parallel to the line BF
   . the line AE is not perpendicular to the line AC
   
   QED.