a_Term C in the carrier of C ;
then A1: a_Term C <> the carrier of C ;
A2: (x -term C) . {} = [x,(a_Term C)] by TREES_4:3;
a_Term C nin { the carrier of C} by A1, TARSKI:def 1;
hence (x -term C) . {} nin [: the carrier' of C,{ the carrier of C}:] by A2, ZFMISC_1:87; :: according to ABCMIZ_1:def 27 :: thesis: verum