take a_Term ; :: according to PBOOLE:def 12 :: thesis: ( a_Term in the carrier of C & not (MSVars C) . a_Term is empty )
the carrier of C = {a_Type,an_Adj,a_Term} by Def9;
hence a_Term in the carrier of C by ENUMSET1:def 1; :: thesis: not (MSVars C) . a_Term is empty
thus not (MSVars C) . a_Term is empty by Def25; :: thesis: verum