thus card (INT.Group n) = card (Segm n) by Th76
.= n ; :: thesis: verum