theorem Th42: :: YELLOW_7:42

for S, T being non empty RelStr
for f being Function of S,T
for g being Function of (S opp),(T opp) 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 ) )