theorem :: ABCMIZ_1:87

for C being initialized ConstructorSignature
for x being variable holds vars (x -term C) = {x} \/ (vars x)