reconsider t = [c, the carrier of C] -tree p as expression of C by A1, A2, Th51;
t . {} = [c, the carrier of C] by TREES_4:def 4;
then t . {} in [: the carrier' of C,{ the carrier of C}:] by ZFMISC_1:106;
hence [c, the carrier of C] -tree p is compound expression of C by Def27; :: thesis: verum