Miquel's Theorem

Miquel:=proc() local A,P,C,t,i,s,O,R:

for i from 0 to 3 do   A[i]:= ParamCircle(O,R,t[i]):   od:
for i from 0 to 3 do   C[i]:= ParPtPerBisect (A[i],A[(i+1) mod 4],s[i]):   od:
for i from 0 to 3 do   P[i]:= MirRefPtLe (A[i],Le(C[(i-1) mod 4],C[i])):   od:

Concyclic(P[0],P[1],P[2],P[3]):

end: