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:
U:=proc(A,B,C):H(A,B)*H(B,C)*H(C,A):end:
S:=proc() local K,t,i:K:={seq(P(t[i]),i=1..4)}:T(seq(U(op(K minus {P(t[i])})),i=1..4)):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 .