:: deftheorem Def7 defines UnContinuous TOPGRP_1:def 7 :
for G being non empty Group-like associative TopGrStr holds
( G is UnContinuous iff inverse_op G is continuous );