By Shalosh B. EKHAD   [c/o zeilberg at math dot rutgers dot edu]

#Copy and paste into a Maple session and get: true
H:=proc(A,B):(A[1]-B[1])^2+(A[2]-B[2])^2: end:
P:=proc(t):[(t+1/t)/2,(t-1/t)/2/I]:end:
T:=proc(A,B,C,D):
evalb(expand(((A+B-C-D)^2-4*(A*B+C*D))^2-64*A*B*C*D)=0):end:
S:=proc() local t1,t2,t3,t4,A,B,C,D,a,b,c,d,p,q: 
A:=P(t1): B:=P(t2):C:=P(t3): D:=P(t4):
a:=H(A,B):b:=H(B,C):c:=H(C,D):d:=H(D,A):p:=H(A,C):q:=H(B,D):
T(a*b*p,c*d*p,b*c*q,a*d*q):end: print(S()):
#--------------end Maple Code

---

Added Oct. 17, 2004: Sergey Sadov informed me that while this beautiful theorem escaped the notice of geometers for a long time, it did appear in the literature before, and has a fairly short human proof:
M.A.Rashid and A.O.Ajibade, Two conditions for a quadrilateral to be cyclic expressed in terms of the lengths of its sides. Int.J.Math.Educ.Sci.Technol., 2003, Vol. 34, No 5, 739--742.

---

Personal Journal of Ekhad and Zeilberger .