:: deftheorem defines invrat BINOP_2:def 14 :
for b₁ being UnOp of RAT holds
( b₁ = invrat iff for w being Rational holds b₁ . w = w " );