:: deftheorem defines invreal BINOP_2:def 8 :
for b₁ being UnOp of REAL holds
( b₁ = invreal iff for r being Real holds b₁ . r = r " );