Description: This theorem can be used to shorten G = hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013)