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;
A0: NonTerminals (DTConMSA (MSVars C)) = [:the carrier' of C,{the carrier of C}:] by ThTNT;

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 set such that
A1: ( a in the carrier' of C & b in {the carrier of C} & t = [a,b] ) by A0, ZFMISC_1:def 2;
reconsider a = a as OperSymbol of C by A1;
( b = the carrier of C & ( a is constructor or not a is constructor ) ) by A1, 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] ) by A1, CNSTR2; :: 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 A0, ZFMISC_1:106; :: thesis: verum