Eight Point Circle Exists Theorem

EightPointCircleExists:=proc() local A,B,C,D,e,f,g,h,a,b,c,d,a1,b1,c1,d1:

A:=[0,-e]:   B:=[f,0]:   C:=[0,g]:   D:=[-h,0]:

a:=MidPt (A,B):   b:=MidPt(B,C):   c:=MidPt(C,D):   d:=MidPt(D,A):

a1:=Ft (a, Le (C,D)):   b1:= Ft (b,Le (D,A)):   c1:=Ft (c, Le (A,B)):   d1:=Ft (d,Le (B,C)):

Concyclic (a,b,c,d,a1,b1,c1,d1):

end: