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:87; :: thesis: verum