let k, n be Nat; :: thesis: ( n >= 8 implies ex m being Multiple of 3 st
( m in seq (k,n) & m is odd ) )
assume A1: n >= 8 ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

per cases ( 3 divides k or 3 divides k + 1 or 3 divides k + 2 ) by NUMBER06:18;

suppose 3 divides k ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

then A2: k is Multiple of 3 by Def15;

per cases ( k is even or k is odd ) ;

suppose A3: k is even ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

reconsider m = k + (1 * (2 + 1)) as Multiple of 3 by A2, Th58;
take m ; :: thesis: ( m in seq (k,n) & m is odd )
A4: 1 + k <= (k + 1) + 2 by NAT_1:12;
3 <= n by A1, XXREAL_0:2;
then k + 3 <= k + n by XREAL_1:6;
hence m in seq (k,n) by A4; :: thesis: m is odd
m = (k + 2) + 1 ;
hence m is odd by A3; :: thesis: verum

end;

suppose A5: k is odd ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

reconsider m = k + (2 * (2 + 1)) as Multiple of 3 by A2, Th58;
take m ; :: thesis: ( m in seq (k,n) & m is odd )
A6: 1 + k <= (k + 1) + 5 by NAT_1:12;
6 <= n by A1, XXREAL_0:2;
then k + 6 <= k + n by XREAL_1:6;
hence m in seq (k,n) by A6; :: thesis: m is odd
thus m is odd by A5; :: thesis: verum

end;

end;

end;

suppose 3 divides k + 1 ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

then A7: k + 1 is Multiple of 3 by Def15;

per cases ( k is even or k is odd ) ;

suppose A8: k is even ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

reconsider m = (k + 1) + (2 * (2 + 1)) as Multiple of 3 by A7, Th58;
take m ; :: thesis: ( m in seq (k,n) & m is odd )
A9: 1 + k <= (k + 1) + 6 by NAT_1:12;
7 <= n by A1, XXREAL_0:2;
then k + 7 <= k + n by XREAL_1:6;
hence m in seq (k,n) by A9; :: thesis: m is odd
thus m is odd by A8; :: thesis: verum

end;

suppose A10: k is odd ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

reconsider m = (k + 1) + (1 * (2 + 1)) as Multiple of 3 by A7, Th58;
take m ; :: thesis: ( m in seq (k,n) & m is odd )
A11: 1 + k <= (k + 1) + 3 by NAT_1:12;
4 <= n by A1, XXREAL_0:2;
then k + 4 <= k + n by XREAL_1:6;
hence m in seq (k,n) by A11; :: thesis: m is odd
m = k + (2 * 2) ;
hence m is odd by A10; :: thesis: verum

end;

end;

end;

suppose 3 divides k + 2 ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

then A12: k + 2 is Multiple of 3 by Def15;

per cases ( k is even or k is odd ) ;

suppose A13: k is even ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

reconsider m = (k + 2) + (1 * (2 + 1)) as Multiple of 3 by A12, Th58;
take m ; :: thesis: ( m in seq (k,n) & m is odd )
A14: 1 + k <= (k + 1) + 4 by NAT_1:12;
5 <= n by A1, XXREAL_0:2;
then k + 5 <= k + n by XREAL_1:6;
hence m in seq (k,n) by A14; :: thesis: m is odd
m = (k + (2 * 2)) + 1 ;
hence m is odd by A13; :: thesis: verum

end;

suppose A15: k is odd ; :: thesis: ex m being Multiple of 3 st
( m in seq (k,n) & m is odd )

reconsider m = (k + 2) + (2 * (2 + 1)) as Multiple of 3 by A12, Th58;
take m ; :: thesis: ( m in seq (k,n) & m is odd )
A16: 1 + k <= (k + 1) + 7 by NAT_1:12;
k + 8 <= k + n by A1, XREAL_1:6;
hence m in seq (k,n) by A16; :: thesis: m is odd
thus m is odd by A15; :: thesis: verum

end;

end;

end;

end;