A1: the carrier of S in {the carrier of S} by TARSKI:def 1;
NonTerminals (DTConOSA X) = [:the carrier' of S,{the carrier of S}:] by Th3;
hence OSSym o,X is NonTerminal of (DTConOSA X) by A1, ZFMISC_1:106; :: thesis: verum