( c in Modes \/ Attrs or c in Funcs )
by XBOOLE_0:def 3;
then
( c in Modes or c in Attrs or c in Funcs )
by XBOOLE_0:def 3;
then
( c `1 in {a_Type } or c `1 in {an_Adj } or c `1 in {a_Term } )
by MCART_1:10;
then
( c `1 = a_Type or c `1 = an_Adj or c `1 = a_Term )
by TARSKI:def 1;
hence
vars c is Element of {a_Type ,an_Adj ,a_Term }
by ENUMSET1:def 1; verum