:: deftheorem defines subexpression ABCMIZ_A:def 7 :
for C being initialized ConstructorSignature
for e, b₃ being expression of C holds
( b₃ is subexpression of e iff b₃ in Subtrees e );