A1: the carrier of S in {the carrier of S} by TARSKI:def 1;
A2: NonTerminals (DTConMSA V) = [:the carrier' of S,{the carrier of S}:] by MSAFREE:6;
Sym o,V = [o,the carrier of S] by MSAFREE:def 11;
hence Sym o,V is NonTerminal of (DTConMSA V) by A2, A1, ZFMISC_1:106; :: thesis: verum