:: deftheorem Def35 defines inverse-closed AIMLOOP:def 37 :
for X being functional set holds
( X is inverse-closed iff for f being Element of X st f in X holds
f " in X );