for n being natural number holds
( not n divides 3 or n = 1 or n = 3 )

proof

let n be natural number ; :: thesis: ( not n divides 3 or n = 1 or n = 3 )
assume A1: n divides 3 ; :: thesis: ( n = 1 or n = 3 )
then A2: n <> 0 by INT_2:3;
n <= 3 by A1, NAT_D:7;
then ( n < 2 + 1 or n = 3 ) by XXREAL_0:1;
then ( n <= 2 or n = 3 ) by NAT_1:13;
then ( n < 1 + 1 or n = 2 or n = 3 ) by XXREAL_0:1;
then ( n <= 1 or n = 2 or n = 3 ) by NAT_1:13;
then A3: ( n < 1 or n = 1 or n = 2 or n = 3 ) by XXREAL_0:1;
n <> 2

proof

assume A4: n = 2 ; :: thesis: contradiction
3 mod 2 = ((2 * 1) + 1) mod 2
.= 1 mod 2 by NAT_D:21
.= 1 by NAT_D:24 ;
hence contradiction by A1, A4, Th6; :: thesis: verum

end;

hence ( n = 1 or n = 3 ) by A2, A3, NAT_1:14; :: thesis: verum

end;

hence 3 is prime by INT_2:def 5; :: thesis: verum