the carrier of G = (Terminals G) \/ (NonTerminals G) by LANG1:1;
hence NonTerminals G is Subset of G by XBOOLE_1:7; :: thesis: verum