support (min (b1,b2)) c= (support b1) \/ (support b2) by Th17;
hence support (min (b1,b2)) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum