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