Hi James,
To answer your first question, notice the [] (Box) in the formula Spec
and look up that symbol in the index of "Specifying Systems".
TLC ignores THEOREMs. The TLAPS proof system allows you to prove
them, but you're probably not ready for that.
I suggest looking at the TLA+ Hyperbook to find out about using TLC.
(There's a link to it on the TLA+ Web page.)
Good luck,
Leslie