theorem :: MONOID_0:41

for G being non empty strict SubStr of <REAL,+> holds
( G = INT.Group iff the carrier of G = INT ) by Th26, GR_CY_1:def 3;