L1:
        if collinear(A,B,C)
            [ABC]=0

    L2:
        if parallel(PQ,AB)
            [PAB]=[QAB]

    L3:
        for any four points A,B,C,D
            [ABC]=[DBC]+[ADC]+[ABD]

    L4:
        if collinear(A,B,C,D) , P does not lie on AB
            CD/AB=[PCD]/[PAB]

    L5:
        if collinear(A,B,M) and collinear(P,Q,M)
            PM/QM=[PAB]/[QAB]

    L6:
        if collinear(P,Q,R) then for any two points A,B
            [RAB]= (PR/PQ) *[QAB] + (RQ/PQ)*[PAB]

    L7:
        if collinear(A,B,P,Q)
            (APAB) + (PB/AB) =1

Lemmas used in the full angle method:

    L1:
        if parallel(A,B,P,Q)
                   [AB,PQ]=0

    L2:
        perpendicular(A,B,P,Q)
            [AB,PQ]=90

    L3:
        if collinear(X,P,Q)
            [AB,PQ]=[AB,PX]

    L4:
        if parallel(PX,UV)
               [AB,PX]=[AB,UV]

    L5:
        if XA=XB
            [AX,AB]=[AB,XB]

    L6:
        if cyclic(A,B,C,D)
            [AD,CD]=[AB,CB]

    L7:
        if O is circumcenter of ABC and M is the midpoint of AB
            [AO,OM]=[AC,BC]

    L8:
        if MA=MB  and cyclic(A,B,P,M)
            [PA,PM]=[PM,PB]

    L9:
        for any line UV
            [AB,CD]=[AB,UV]+[UV,CD]
 

   Rules used in the forward chaining:

     R1:
        if parallel(l1,l2) and parallel(l2,l3)        (l denotes line)
            parallel(l1,l3)

    R2:
        if perpendicular(l1,l2)
            perpendicular(l2,l3) <=>  parallel(l1,l3)

    R3:
        if O is midpoint of AC
             perpendicular(AB,BC) <=> O is circumcenter of triangle ABC

    R4:
        if perpendicular(PA,PB)
            perpendicular(QA,QB) <=> cyclic (A,B,P,Q)

    R5:
        if M,N are the midpoints of AB,AC
            parallel(MN,BC)

    R6:
        if parallel(AB,AC)
            collinear(A,B,C)

    R7:
        OA=OB <=> [OA,AB]=[AB,OB]

    R8:
        if [AB,AC]=[DB,DC]
            concyclic(A,B,C,D)

    R9:
        if MA=MB and cyclic(A,B,P,M)
            [PA,PM]=[PM,PB]