support (max b1,b2) c= (support b1) \/ (support b2) by Th18;
hence support (max b1,b2) is finite ; :: according to POLYNOM1:def 8 :: thesis: verum