NonTerminals G c= the carrier of G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NonTerminals G or a in the carrier of G )
assume a in NonTerminals G ; :: thesis: a in the carrier of G
then ex s being Symbol of G st
( a = s & ex n being FinSequence st s ==> n ) ;
hence a in the carrier of G ; :: thesis: verum

end;

hence NonTerminals G is non empty Subset of G by Def11; :: thesis: verum