Pascal's Theorem:

If three points on a line are joined to three points on another line such that two pairs of lines are parallel, then the third pair is also parallel

Machine Input :

Point Order : ABPQCR
Hypotheses : coll(ABC) coll(PQR) para(AQBR) para(BPCQ)
Conjecture : para(CRAP)

Machine Output:

We can equivalently prove that :-

1.0[RCA]
--------------------------   =  1
1.0[RCP]

Proof:

   1.0[RCA]
   ---------------------
   1.0[RCP]

      By putting [RCP] = [QPB]-[RPB]+[RCB]

   1.0[RCA]
=  ---------------------
   1.0([QPB]-[RPB]+[RCB])

      By putting [RPB] = [QPB]-[RBA]

   1.0[RCA]
=  ---------------------
   1.0([RBA]+[RCB])

      By putting [RCB] = -[RBA]+[RCA]

   1.0
=  ---------------------
   1.0

Compute Time=0.121 seconds