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;
A1: Terminals (DTConMSA (MSVars C)) = Union (coprod (MSVars C)) by Th120;
A2: dom (MSVars C) = the carrier of C by PARTFUN1:def 2;
A3: the carrier of C = {a_Type,an_Adj,a_Term} by Def9;
A4: (MSVars C) . a_Type = {} by Def25;
A5: (MSVars C) . an_Adj = {} by Def25;
A6: (MSVars C) . a_Term = Vars by Def25;

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

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

end;

given x being variable such that A11: t = [x,(a_Term C)] ; :: thesis: t in Terminals (DTConMSA (MSVars C))
A12: t `1 = x by A11;
t `2 = a_Term by A11;
hence t in Terminals (DTConMSA (MSVars C)) by A1, A2, A6, A11, A12, CARD_3:22; :: thesis: verum