theorem :: MONOID_0:42

for x being set holds
( x is Element of INT.Group iff x is Integer ) by GR_CY_1:def 3, INT_1:def 2;