theorem Th123: :: ABCMIZ_1:123

for C being initialized ConstructorSignature
for t being set holds
( t in NonTerminals (DTConMSA (MSVars C)) iff ( t = [(ast C), the carrier of C] or t = [(non_op C), the carrier of C] or ex c being constructor OperSymbol of C st t = [c, the carrier of C] ) )