Here the first inclusion follows because a SAT instance can trivially be written as an equivalent ETR instance.
The second inclusion is highly non-trivial and was first proven by Canny in his seminal paper [1]}.
