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