let C be initialized ConstructorSignature; :: thesis: for e being expression of C holds e is subexpression of e
let e be expression of C; :: thesis: e is subexpression of e
thus e in Subtrees e by TREES_9:11; :: according to ABCMIZ_A:def 7 :: thesis: verum