let n be Nat; :: thesis: ( not 6 divides n iff ex k being Nat st
( n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) )

consider K being Nat such that
A1: ( n = 6 * K or n = (6 * K) + 1 or n = (6 * K) + 2 or n = (6 * K) + 3 or n = (6 * K) + 4 or n = (6 * K) + 5 ) by Th26;
thus ( not 6 divides n implies ex k being Nat st
( n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) ) by A1; :: thesis: ( ex k being Nat st
( n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) implies not 6 divides n )

given k being Nat such that A2: ( n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) ; :: thesis: not 6 divides n
given t being Nat such that A3: n = 6 * t ; :: according to NAT_D:def 3 :: thesis: contradiction
per cases ( n = (6 * k) + 1 or n = (6 * k) + 2 or n = (6 * k) + 3 or n = (6 * k) + 4 or n = (6 * k) + 5 ) by A2;
suppose n = (6 * k) + 1 ; :: thesis: contradiction
end;
suppose n = (6 * k) + 2 ; :: thesis: contradiction
end;
suppose n = (6 * k) + 3 ; :: thesis: contradiction
end;
suppose n = (6 * k) + 4 ; :: thesis: contradiction
end;
suppose n = (6 * k) + 5 ; :: thesis: contradiction
end;
end;