reconsider a = 2 as Prime by XPRIMES1:2;
reconsider b = 5 as Prime by XPRIMES1:5;
reconsider c = 53 as Prime by XPRIMES1:53;
take a ; :: according to NUMBER07:def 2 :: thesis: ex b, c being Prime st
( a,b,c are_mutually_distinct & (23 |^ 2) + 1 = (a * b) * c )
take b ; :: thesis: ex c being Prime st
( a,b,c are_mutually_distinct & (23 |^ 2) + 1 = (a * b) * c )
take c ; :: thesis: ( a,b,c are_mutually_distinct & (23 |^ 2) + 1 = (a * b) * c )
thus ( a,b,c are_mutually_distinct & (23 |^ 2) + 1 = (a * b) * c ) by Th52; :: thesis: verum