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