for n being odd Nat holds
( not n <= 4 or n = 1 or n = 3 )