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