theorem :: ABCMIZ_A:16

for C being initialized standardized ConstructorSignature
for e being expression of C holds
( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C )