set X = MSVars C;
let x be object ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in (MSVars C) " {{}} or x in rng the ResultSort of C )
assume A23: x in (MSVars C) " {{}} ; :: thesis: x in rng the ResultSort of C
then A24: x in dom (MSVars C) by FUNCT_1:def 7;
A25: (MSVars C) . x in {{}} by A23, FUNCT_1:def 7;
x in the carrier of C by A24;
then x in {a_Type,an_Adj,a_Term} by Def9;
then A26: ( x = a_Type or x = an_Adj or x = a_Term ) by ENUMSET1:def 1;
A27: (MSVars C) . x = {} by A25, TARSKI:def 1;
A28: the ResultSort of C . (ast C) = a_Type by Def9;
the ResultSort of C . (non_op C) = an_Adj by Def9;
hence x in rng the ResultSort of C by A26, A27, A28, Def25, FUNCT_2:4; :: thesis: verum