theorem :: YELLOW_7:41

for S, T being non empty RelStr
for f being Function of S,(T opp)
for g being Function of (S opp),T st f = g holds
( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) )