Nine-Point Circle Exists Theorem

NinePointCircleExists:=proc() local A,B,C,O,D,E,F,G,H,I,K,L,M:

D:=Ft(A,Le(B,C)):   E:=Ft(B,Le(A,C)):   F:=Ft(C,Le(A,B)):   G:=MidPt(A,B):  H:= MidPt(A,C):   I:=MidPt(B,C):

O:=Orthocenter(A,B,C): 

K:=MidPt(O,A):   L:= MidPt(O,B):   M:=MidPt(O,C):

Concyclic(D,E,F,G,H,I,K,L,M):

end: