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