;;----------------------------------------------------------------
;; Encoding of the Pappus theorem in the formalism
;; implemented in the PROVER package.
;;----------------------------------------------------------------
(prove-theorem
 ((collinear X Y Z)
  (collinear X P V)
  (collinear U P Y)
  (collinear Y R W)
  (collinear Z R V)
  (collinear U Q Z)
  (collinear X Q W)
  (collinear U V W))
 ((collinear P Q R))
 :order #'grevlex>)