given a, b, c being Prime such that a,b,c are_mutually_distinct and
A1: (12 |^ 2) + 1 = (a * b) * c ; :: according to NUMBER07:def 2 :: thesis: contradiction
12 |^ 2 = 12 * 12 by WSIERP_1:1;

per cases then ( ( a * b = 1 & c = 145 ) or ( a * b = 5 & c = 29 ) or ( a * b = 29 & c = 5 ) or ( a * b = 145 & c = 1 ) ) by A1, Th34;

suppose ( a * b = 1 & c = 145 ) ; :: thesis: contradiction

hence contradiction by XPRIMES0:145; :: thesis: verum

end;

suppose ( a * b = 5 & c = 29 ) ; :: thesis: contradiction

hence contradiction by XPRIMES1:5; :: thesis: verum

end;

suppose ( a * b = 29 & c = 5 ) ; :: thesis: contradiction

hence contradiction by XPRIMES1:29; :: thesis: verum

end;

suppose ( a * b = 145 & c = 1 ) ; :: thesis: contradiction

hence contradiction by XPRIMES0:1; :: thesis: verum

end;

end;