:: deftheorem Def7 defines UnContinuous GROUP_1A:def 46 :
for G being non empty add-associative addGroup-like TopaddGrStr holds
( G is UnContinuous iff add_inverse G is continuous );