let C be 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] ) )
let t be set ; ( 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 ( ( 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))
;
( 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;
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; verum