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:129;
hence [c,the carrier of C] -tree p is compound expression of C by Def27; :: thesis: verum