:: deftheorem defines opp WAYBEL34:def 3 :
for S, T being RelStr
for f being Function of the carrier of S, the carrier of T holds f opp = f;