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

per cases then ( ( a * b = 1 & c = 50 ) or ( a * b = 2 & c = 25 ) or ( a * b = 5 & c = 10 ) or ( a * b = 10 & c = 5 ) or ( a * b = 25 & c = 2 ) or ( a * b = 50 & c = 1 ) ) by A2, Th30;

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

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

end;

suppose ( a * b = 2 & c = 25 ) ; :: thesis: contradiction

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

end;

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

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

end;

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

hence contradiction by A1, Th27; :: thesis: verum

end;

suppose ( a * b = 25 & c = 2 ) ; :: thesis: contradiction

then ( ( a = 1 & b = 25 ) or ( a = 5 & b = 5 ) or ( a = 25 & b = 1 ) ) by Th28;
hence contradiction by A1, XPRIMES0:25; :: thesis: verum

end;

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

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

end;

end;