ATP verification, obtaining sufficient conditions

This applet will load slower than usual GeoGebra applets. Please allow at least 20 seconds for loading. Pappus' hexagon theorem claims collinearity of certain intersection points.
  1. In Steps 1-3 the construction is drawn. In Step 4 three intersection points are highlighted (in pink color). They are collinear (Step 5, pink line). You will be able to switch this pink line off (Step 6) and on again.
  2. In Step 7-8 another triplet of collinear points is drawn (in purple). In fact, there are 6 triplets of such points (Step 9). They are called "Pappus lines".
  3. Go to Step 10 now. You can obtain a sufficient condition (by using the ProveDetails command in GeoGebra) for the pink line to exist. The meaning of this condition is "if all of the conditions are false, then the line exists". If there is only one condtion, then, of course it means "if the condition is false, then the line exists". "..." means that there are some mathematical conditions, but GeoGebra cannot convert them into human readable format.
  4. Step 11 shows another sufficient condition for the purple line, too.
  5. Enable all (or some) other checkboxes to obtain sufficient conditions for the other Pappus lines. Note that conditions differ.
  6. Reload this page as an HTML5 applet (below). This will take a while since HTML5 computations can be slow. Allow 1 minute for the page to load. Then compare the results in the sufficient conditions. The reason of the difference is that the used mathematical algorithm can be somewhat different.