Symbolic Coding Theorem for the Smale Horseshoe