take <*b*> ; :: thesis: b = Sum <*b*>
thus b = Sum <*b*> by Th23; :: thesis: verum