given a, b, c being Prime such that a,b,c are_mutually_distinct and
A1: (0 |^ 2) + 1 = (a * b) * c ; :: according to NUMBER07:def 2 :: thesis: contradiction
( a * b = 1 & c = 1 ) by A1, NAT_1:15;
hence contradiction ; :: thesis: verum