theorem Th7: :: NUMBER10:7

for a, n being Nat holds
( a <= (6 * n) + 1 iff a in <=6n+1 n )