(non_op C) term a = [non_op, the carrier of C] -tree <*a*> by Th43;
then ((non_op C) term a) . {} = [(non_op C), the carrier of C] by TREES_4:def 4;
hence ((non_op C) term a) . {} in [: the carrier' of C,{ the carrier of C}:] by ZFMISC_1:106; :: according to ABCMIZ_1:def 27 :: thesis: verum