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 9;
hence Sym (o,V) is NonTerminal of (DTConMSA V) by A2, A1, ZFMISC_1:87; :: thesis: verum