let a, n be Nat; :: thesis: ( a <= (6 * n) + 1 iff a in <=6n+1 n )
thus ( a <= (6 * n) + 1 implies a in <=6n+1 n ) ; :: thesis: ( a in <=6n+1 n implies a <= (6 * n) + 1 )
assume a in <=6n+1 n ; :: thesis: a <= (6 * n) + 1
then ex b being Nat st
( a = b & b <= (6 * n) + 1 ) ;
hence a <= (6 * n) + 1 ; :: thesis: verum