Miquel Point Theorem:
Four lines form four triangles. Prove that the circumcircles of the four triangles pass through a common point.

Machine Input:

Point order : ABCDEPQ

Hypothesis: coll(GDC) coll(GDA) coll(BCE) coll(ADE) cyclic(ABEF) cyclic(CDEF)

Conclusion: cyclic (ADFG)

Machine output:

- [DQ,AQ] + [PD,PA]
=   - [DQ,AQ] + [PD,BA]
        ( because collinear(P,A,B) => [PD,PA] = [PD,BA] )
=   - [DQ,AQ] + [DC,BA]
        ( because collinear(P,D,C) => [PD,BA] = [DC,BA] )
=   - [DQ,AQ] + [DC,BE] - [BA,BE]
        ( because [DC,BA] = [DC,BE] + -1.0[BA,BE])
=   - [DQ,AQ] + [DC,BE] - [AQ,EQ]
        ( because cyclic(B,A,E,Q) => -1.0[BA,BE] = -1.0[AQ,EQ] )
=   - [DQ,AQ] + [DC,CE] - [AQ,EQ]
        ( because collinear(B,E,C) => [DC,BE] = [DC,CE] )
=   - [DQ,AQ] + [DQ,EQ] - [AQ,EQ]
        ( because cyclic(D,C,E,Q) => [DC,CE] = [DQ,EQ] )
= 0.0
        ( because -1.0[DQ,AQ] = -1.0[DQ,EQ]+[AQ,EQ], simplifying )