Johnson's Theorem

Johnson:=proc() local C,t,i,R,P,O:

for i from 0 to 2 do   C[i]:= ParamCircle(O,R,t[i]):   od:

for i from 0 to 2 do   P[i]:= MirRefPtLe (O, Le (C[i],C[i+1 mod 3]) ) :   od:

ItIsZero(Radius (Ce (P[0],P[1],P[2]))^2   -   R^2):

end: