theorem :: NUMBER05:44
for p, q, r, s, t being Prime holds
( not (p ^2) + (q ^2) = ((r ^2) + (s ^2)) + (t ^2) or p is even or q is even or r is even or s is even or t is even ) ;