support (b1 + b2) = (support b1) \/ (support b2) by Th37;
hence support (b1 + b2) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum