the carrier of (center R) c= the carrier of R by Th17;
hence center R is finite ; :: thesis: verum