let x be set ; :: according to GRCAT_1:def 17 :: thesis: ( x in GroupObjects UN implies x is strict AddGroup )
thus ( x in GroupObjects UN implies x is strict AddGroup ) by Th30; :: thesis: verum