given a, b, c being Prime such that a,b,c are_mutually_distinct and
A1: (4 |^ 2) + 1 = (a * b) * c ; :: according to NUMBER07:def 2 :: thesis: contradiction
4 |^ 2 = 4 * 4 by WSIERP_1:1;
then ( ( a * b = 1 & c = 17 ) or ( a * b = 17 & c = 1 ) ) by A1, Th26, XPRIMES1:17;
hence contradiction by NAT_1:15, XPRIMES0:1; :: thesis: verum