(* This figure, drawn by Lyle Ramshaw, 
   demonstrates a theorem of projective geometry. 
   The complete quadrilateral shown by the four 
   black lines in the lower half of the figure) 
   has three pairs of opposite vertices. Draw 
   lines from these six vertices through a point 
   on a conic section (point "O" in the figure). 
   Each line intersects the conic section a second 
   time. The three chords determined by the three 
   pairs of second intersections are concurrent. *)

CONST M = 150;

PRIVATE PRED P(X, Y, a, b) IS 
  13 * (X * X + 4 * Y * Y) * a = 
    2 * b * (24 * Y - 5 * X) * M 
END;

PRED Resid(p, P, O) IS 
  (E X = CAR(P) - CAR(O), Y = CDR(P) - CDR(O), 
     x = CAR(p) - CAR(O), y = CDR(p) - CDR(O) :: 
    P(X, Y, y, Y) AND P(X, Y, x, X)) 
END;

PROC Connect(p, q, r) IS 
  PS.MoveTo(p); 
  PS.LineTo(q); 
  PS.LineTo(r); 
  PS.Close(); 
  PS.Stroke() 
END;

PROC DrawEllipse(O) IS 
  VAR c, dx, dy, b IN 
    dx := -5 * M / 13; 
    dy := 6 * M / 13; 
    c := R2.Plus(O, (dx, dy)); 
    b := R2.Plus(c, (M, 0)); 
    Ellipse.DrawEcc(c, b, 0.5) 
  END 
END;

PROC Cmd0() IS 
  IF 
    VAR 
      O = (65.13, 43.99), A1 = (-191.6, -58.4), 
      A2 ~ (-47.693813, -47.866493), B3 = (160.6, -32.62), 
      B2 ~ (-48.898727, -103.25245), A3 = (160.6, -169.1), 
      B1 = (12.12, -82.68), a1 ~ (129.60846, 69.705536), 
      a2 ~ (157.02144, 118.80422), a3 ~ (0.5462392, 188.1416), 
      b1 ~ (115.80404, 165.07812), b2 ~ (143.33302, 144.97162), 
      b3 ~ (-91.43163, 169.62305), con ~ (109.296555, 210.03734) 
    IN 
      Resid(a1, A1, O) AND 
      Resid(a2, A2, O) AND 
      Resid(a3, A3, O) AND 
      Resid(b1, B1, O) AND 
      Resid(b2, B2, O) AND 
      Resid(b3, B3, O) AND 
      Geometry.Colinear(B1, B2, B3) AND 
      Geometry.Colinear(A1, B2, A3) AND 
      Geometry.Colinear(A1, A2, B3) AND 
      Geometry.Colinear(A2, B1, A3) AND 
      Geometry.Colinear(a1, b1, con) AND 
      Geometry.Colinear(a2, b2, con) -> 
        PS.SetWidth(1.5); 
        DrawEllipse(O); 
        PS.Stroke(); 
        Connect(A1, A2, B3); 
        Connect(A1, B2, A3); 
        Connect(B1, A2, A3); 
        Connect(B1, B2, B3); 
        PS.SetColor(Color.Red); 
        Connect(A1, O, a1); 
        Connect(B1, O, b1); 
        Connect(a1, b1, con); 
        PS.SetColor([0, 0.7, 0]); 
        Connect(A2, O, a2); 
        Connect(B2, O, b2); 
        Connect(a2, b2, con); 
        PS.SetColor(Color.Blue); 
        Connect(A3, O, a3); 
        Connect(B3, O, b3); 
        Connect(a3, b3, con) 
    END 
  FI 
END;