theorem :: ABCMIZ_A:23

for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )