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