support (b1 -' b2) c= support b1 by Th38;
hence support (b1 -' b2) is finite ; :: according to PRE_POLY:def 8 :: thesis: verum