set t = x -term ;
[x,s] in {[x,s]} by TARSKI:def 1;
then Coim ((x -term),[x,s]) = {{}} by TREES_1:29, FUNCOP_1:14;
hence card (Coim ((x -term),[x,s])) = 1 by CARD_1:30; :: according to MSAFREE5:def 20 :: thesis: verum