let n be Nat; ( not n divides 325 or n = 1 or n = 5 or n = 13 or n = 25 or n = 65 or n = 325 )
assume
n divides 325
; ( n = 1 or n = 5 or n = 13 or n = 25 or n = 65 or n = 325 )
then
n divides 13 * 25
;
then consider a, b being Nat such that
A1:
( a divides 13 & b divides 25 )
and
A2:
n = a * b
by Lem1;
( ( a = 1 or a = 13 ) & ( b = 1 or b = 5 or b = 25 ) )
by A1, Th13, XPRIMES1:13;
hence
( n = 1 or n = 5 or n = 13 or n = 25 or n = 65 or n = 325 )
by A2; verum