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