let n be Nat; :: thesis: ( not n divides 65 or n = 1 or n = 5 or n = 13 or n = 65 )
65 = 5 * 13 ;
hence ( not n divides 65 or n = 1 or n = 5 or n = 13 or n = 65 ) by Lem2, XPRIMES1:5, XPRIMES1:13; :: thesis: verum