set G = INT.Group 2;
the carrier of ((1). (INT.Group 2)) = {(1_ (INT.Group 2))} by GROUP_2:def 7
.= {} \/ {0} by GR_CY_1:14
.= succ 0 by ORDINAL1:def 1
.= 1 ;
then the carrier of ((1). (INT.Group 2)) <> the carrier of (INT.Group 2) by ORDINAL1:def 17;
hence not INT.Group 2 is trivial by Th6; :: thesis: verum