degree B = card B ;
hence Sum B is Element of NAT ; :: thesis: verum