given a, b, c being Prime such that
a,b,c are_mutually_distinct
and
A1:
(3 |^ 2) + 1 = (a * b) * c
; NUMBER07:def 2 contradiction
3 |^ 2 = 3 * 3
by WSIERP_1:1;
then
( ( a * b = 1 & c = 10 ) or ( a * b = 2 & c = 5 ) or ( a * b = 5 & c = 2 ) or ( a * b = 10 & c = 1 ) )
by A1, Th27;
hence
contradiction
by XPRIMES1:2, XPRIMES1:5, NAT_1:15, XPRIMES0:1; verum