let C be initialized ConstructorSignature; :: thesis: 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] ) )
let t be set ; :: thesis: ( 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] ) )
set X = MSVars C;
A1: NonTerminals (DTConMSA (MSVars C)) = [: the carrier' of C,{ the carrier of C}:] by Th120;

hereby :: thesis: ( ( 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] ) implies t in NonTerminals (DTConMSA (MSVars C)) )

assume t in NonTerminals (DTConMSA (MSVars C)) ; :: thesis: ( 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] )
then consider a, b being object such that
A2: a in the carrier' of C and
A3: b in { the carrier of C} and
A4: t = [a,b] by A1, ZFMISC_1:def 2;
reconsider a = a as OperSymbol of C by A2;
A5: b = the carrier of C by A3, TARSKI:def 1;
( a is constructor or not a is constructor ) ;
hence ( 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] ) by A4, A5; :: thesis: verum

end;

the carrier of C in { the carrier of C} by TARSKI:def 1;
hence ( ( 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] ) implies t in NonTerminals (DTConMSA (MSVars C)) ) by A1, ZFMISC_1:87; :: thesis: verum