(non_op C) term a = [non_op ,the carrier of C] -tree <*a*> by ThNon;
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:129; :: according to ABCMIZ_1:def 27 :: thesis: verum