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