reconsider a = 3 as Prime by XPRIMES1:3;
reconsider b = 11 as Prime by XPRIMES1:11;
reconsider c = 31 as Prime by XPRIMES1:31;
take a ; :: according to NUMBER08:def 5 :: thesis: ex p2, p3 being Prime st
( a,p2,p3 are_mutually_distinct & (32 |^ 2) - 1 = (a * p2) * p3 )
take b ; :: thesis: ex p3 being Prime st
( a,b,p3 are_mutually_distinct & (32 |^ 2) - 1 = (a * b) * p3 )
take c ; :: thesis: ( a,b,c are_mutually_distinct & (32 |^ 2) - 1 = (a * b) * c )
thus ( a,b,c are_mutually_distinct & (32 |^ 2) - 1 = (a * b) * c ) by Th58; :: thesis: verum