the carrier of (INT.Group 1) = Segm 1 by Th76
.= {0} by ORDINAL3:15 ;
hence INT.Group 1 is trivial ; :: thesis: verum