5 = (2 * 2) + 1 ;
then reconsider a = 5 as odd Prime by XPRIMES1:5;
13 = (2 * 6) + 1 ;
then reconsider b = 13 as odd Prime by XPRIMES1:13;
193 = (2 * 96) + 1 ;
then reconsider c = 193 as odd Prime by XPRIMES1:193;
take a ; :: according to NUMBER07:def 3 :: thesis: ex b, c being odd Prime st
( a,b,c are_mutually_distinct & (112 |^ 2) + 1 = (a * b) * c )
take b ; :: thesis: ex c being odd Prime st
( a,b,c are_mutually_distinct & (112 |^ 2) + 1 = (a * b) * c )
take c ; :: thesis: ( a,b,c are_mutually_distinct & (112 |^ 2) + 1 = (a * b) * c )
thus ( a,b,c are_mutually_distinct & (112 |^ 2) + 1 = (a * b) * c ) by Th57; :: thesis: verum