# Leisenring Theorem
Let(A=[x1,0], B=[x2,0], C=[x3,0], A1=[0,x4], B1=[0,x5], C1=[0,x6], O=[0,0],
    P1=[x7,x8], P2=[x9,x10], P3=[x11,x12], L1=[x13,x14], L2=[x15,x16],
    L3=[x17,x18]):
Leisenring := Theorem(
    [arbitrary(A,B,C,A1,B1,C1), collinear(A,B,C), collinear(A1,B1,C1),
     intersection(A,B1,A1,B,P1), intersection(A,C1,A1,C,P2),
     intersection(B,C1,B1,C,P3), intersection(O,P1,C,C1,L1),
     intersection(O,P2,B,B1,L2), intersection(O,P3,A,A1,L3)],
    collinear(L1,L2,L3),[x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18]);

Remark(
`   See`,
`D. Wang: A New Theorem Discovered by Computer Prover. Journal of Geometry`,
`36 (1989) 173-182.` 
):
