let n be Nat; :: thesis: ( not n divides 9 or n = 1 or n = 3 or n = 9 )
assume A1: n divides 9 ; :: thesis: ( n = 1 or n = 3 or n = 9 )
then n <= 9 by INT_2:27;
then A2: not not n = 0 & ... & not n = 9 ;

now :: thesis: ( not 2 divides 9 & not 4 divides 9 & not 5 divides 9 & not 6 divides 9 & not 7 divides 9 & not 8 divides 9 )

((2 * 4) + 1) mod 2 = 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24 ;
hence not 2 divides 9 ; :: thesis: ( not 4 divides 9 & not 5 divides 9 & not 6 divides 9 & not 7 divides 9 & not 8 divides 9 )
((4 * 2) + 1) mod 4 = 1 mod 4 by NAT_D:21
.= 1 by NAT_D:24 ;
hence not 4 divides 9 by INT_1:62; :: thesis: ( not 5 divides 9 & not 6 divides 9 & not 7 divides 9 & not 8 divides 9 )
((5 * 1) + 4) mod 5 = 4 mod 5 by NAT_D:21
.= 4 by NAT_D:24 ;
hence not 5 divides 9 by INT_1:62; :: thesis: ( not 6 divides 9 & not 7 divides 9 & not 8 divides 9 )
((6 * 1) + 3) mod 6 = 3 mod 6 by NAT_D:21
.= 3 by NAT_D:24 ;
hence not 6 divides 9 by INT_1:62; :: thesis: ( not 7 divides 9 & not 8 divides 9 )
((7 * 1) + 2) mod 7 = 2 mod 7 by NAT_D:21
.= 2 by NAT_D:24 ;
hence not 7 divides 9 by INT_1:62; :: thesis: not 8 divides 9
((8 * 1) + 1) mod 8 = 1 mod 8 by NAT_D:21
.= 1 by NAT_D:24 ;
hence not 8 divides 9 by INT_1:62; :: thesis: verum

end;

hence ( n = 1 or n = 3 or n = 9 ) by A1, A2; :: thesis: verum