# Wang's new theorem (Six-Point Theorem)
Let(O=[0,0], A=[x1,0], B=[x2,0], C=[x3,0], A1=[0,x4], B1=[0,x5], C1=[0,x6],
    P3=[x7,x8], P2=[x9,x10], L3=[x11,x12], L2=[x13,x14], W1=[x15,x16],
    P31=[x17,x18], P21=[x19,x20], L31=[x21,x22], L21=[x23,x24], W2=[x25,x26],
    P311=[x27,x28], P211=[x29,x30], L311=[x31,x32], L211=[x33,x34],
    W3=[x35,x36], P3111=[x37,x38], P2111=[x39,x40], L3111=[x41,x42], 
    L2111=[x43,x44], W4=[x45,x46]):
Wang := Theorem( [arbitrary(A,B,C,A1,B1,C1),
     intersection(B,C1,B1,C,P3), intersection(A,C1,A1,C,P2),
     intersection(O,P3,A,A1,L3), intersection(O,P2,B,B1,L2),
     intersection(P3,P2,L3,L2,W1), intersection(B,B1,C1,A,P31),
     intersection(C,C1,A1,B,P21), intersection(O,P31,C,A1,L31),
     intersection(O,P21,A,B1,L21), intersection(P31,P21,L31,L21,W2),
     intersection(A,B1,C1,C,P311), intersection(A,A1,C1,B,P211),
     intersection(O,P311,B,A1,L311), intersection(O,P211,C,B1,L211),
     intersection(P311,P211,L311,L211,W3), intersection(B,C1,A1,C,P3111),
     intersection(A,C1,B1,C,P2111), intersection(O,P3111,A,B1,L3111),
     intersection(O,P2111,B,A1,L2111), 
     intersection(P3111,P2111,L3111,L2111,W4)],
    [collinear(W1,W2,W3),collinear(W1,W2,W4)],
    [x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, 
     x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, 
     x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46]);

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