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