thus b = Sum <*b*> by Th23; :: according to BAGORD_2:def 8 :: thesis: verum