let C be initialized ConstructorSignature; :: thesis: for t being set holds
( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] )
let t be set ; :: thesis: ( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] )
set X = MSVars C;
A0: Terminals (DTConMSA (MSVars C)) = Union (coprod (MSVars C)) by ThTNT;
A1: dom (MSVars C) = the carrier of C by PARTFUN1:def 4;
A2: the carrier of C = {a_Type ,an_Adj ,a_Term } by CONSTRSIGN;
A3: ( (MSVars C) . a_Type = {} & (MSVars C) . an_Adj = {} & (MSVars C) . a_Term = Vars ) by MSVARS;

hereby :: thesis: ( ex x being variable st t = [x,(a_Term C)] implies t in Terminals (DTConMSA (MSVars C)) )

assume t in Terminals (DTConMSA (MSVars C)) ; :: thesis: ex x being variable st t = [x,(a_Term C)]
then A4: ( t `2 in dom (MSVars C) & t `1 in (MSVars C) . (t `2 ) & t = [(t `1 ),(t `2 )] ) by A0, CARD_3:33;
then A5: ( t `2 = a_Type or t `2 = an_Adj or t `2 = a_Term ) by A1, A2, ENUMSET1:def 1;
then reconsider x = t `1 as variable by A3, A4;
take x = x; :: thesis: t = [x,(a_Term C)]
thus t = [x,(a_Term C)] by A3, A4, A5; :: thesis: verum

end;

given x being variable such that A6: t = [x,(a_Term C)] ; :: thesis: t in Terminals (DTConMSA (MSVars C))
( t `1 = x & t `2 = a_Term ) by A6, MCART_1:7;
hence t in Terminals (DTConMSA (MSVars C)) by A0, A1, A3, A6, CARD_3:33; :: thesis: verum