Let(B = [-x1,0], C = [x1,0], A = [0,x2], P = [x3,x4], Q = [x5,x6]):
ExampleA := Theorem(
    [arbitrary(B,C), equidistance(A,B,A,C), collinear(A,B,P), collinear(A,C,Q),
     reflection(B,Q,A,C), reflection(C,P,A,B)], equidistance(B,Q,C,P), 
    [x2, x3, x4, x5, x6]);
