set X = MSVars C;
let x be set ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in (MSVars C) " {{} } or x in rng the ResultSort of C )
assume x in (MSVars C) " {{} } ; :: thesis: x in rng the ResultSort of C
then A1: ( x in dom (MSVars C) & (MSVars C) . x in {{} } ) by FUNCT_1:def 13;
then x in the carrier of C by PBOOLE:def 3;
then x in {a_Type ,an_Adj ,a_Term } by CONSTRSIGN;
then A2: ( x = a_Type or x = an_Adj or x = a_Term ) by ENUMSET1:def 1;
A3: (MSVars C) . x = {} by A1, TARSKI:def 1;
( the ResultSort of C . (ast C) = a_Type & the ResultSort of C . (non_op C) = an_Adj ) by CONSTRSIGN;
hence x in rng the ResultSort of C by A2, A3, MSVARS, FUNCT_2:6; :: thesis: verum