for r being Real
for X being Subset of REAL holds
( r in X iff 1 / r in Inv X )