x is set by TARSKI:1;
hence b +* (x,n) is finite-support ; :: thesis: verum