let S, T be non empty RelStr ; :: thesis: 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 ) )

let f be Function of S,T; :: thesis: 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 ) )

let g be Function of (S ~),(T ~); :: thesis: ( f = g implies ( ( 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 ) ) )
assume A1: f = g ; :: thesis: ( ( 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 ) )
thus ( f is monotone implies g is monotone ) :: thesis: ( ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) )
proof
assume A2: for x, y being Element of S st x <= y holds
f . x <= f . y ; :: according to WAYBEL_1:def 2 :: thesis: g is monotone
let x, y be Element of (S ~); :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or g . x <= g . y )
assume x <= y ; :: thesis: g . x <= g . y
then ~ y <= ~ x by Th1;
then A3: f . (~ y) <= f . (~ x) by A2;
( (f . (~ x)) ~ = f . (~ x) & (f . (~ y)) ~ = f . (~ y) ) ;
hence g . x <= g . y by ; :: thesis: verum
end;
thus ( g is monotone implies f is monotone ) :: thesis: ( f is antitone iff g is antitone )
proof
assume A4: for x, y being Element of (S ~) st x <= y holds
g . x <= g . y ; :: according to WAYBEL_1:def 2 :: thesis: f is monotone
let x, y be Element of S; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or f . x <= f . y )
assume x <= y ; :: thesis: f . x <= f . y
then y ~ <= x ~ by LATTICE3:9;
then A5: g . (y ~) <= g . (x ~) by A4;
( ~ (g . (x ~)) = g . (x ~) & ~ (g . (y ~)) = g . (y ~) ) ;
hence f . x <= f . y by A1, A5, Th1; :: thesis: verum
end;
thus ( f is antitone implies g is antitone ) :: thesis: ( g is antitone implies f is antitone )
proof
assume A6: for x, y being Element of S st x <= y holds
for a, b being Element of T st a = f . x & b = f . y holds
a >= b ; :: according to WAYBEL_0:def 5 :: thesis: g is antitone
let x, y be Element of (S ~); :: according to WAYBEL_0:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of (T ~) holds
( not b1 = g . x or not b2 = g . y or b2 <= b1 ) )

assume x <= y ; :: thesis: for b1, b2 being Element of the carrier of (T ~) holds
( not b1 = g . x or not b2 = g . y or b2 <= b1 )

then ~ y <= ~ x by Th1;
then A7: f . (~ y) >= f . (~ x) by A6;
( (f . (~ x)) ~ = f . (~ x) & (f . (~ y)) ~ = f . (~ y) ) ;
hence for b1, b2 being Element of the carrier of (T ~) holds
( not b1 = g . x or not b2 = g . y or b2 <= b1 ) by ; :: thesis: verum
end;
thus ( g is antitone implies f is antitone ) :: thesis: verum
proof
assume A8: for x, y being Element of (S opp) st x <= y holds
for a, b being Element of (T opp) st a = g . x & b = g . y holds
a >= b ; :: according to WAYBEL_0:def 5 :: thesis: f is antitone
let x, y be Element of S; :: according to WAYBEL_0:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b2 <= b1 ) )

assume x <= y ; :: thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b2 <= b1 )

then y ~ <= x ~ by LATTICE3:9;
then A9: g . (y ~) >= g . (x ~) by A8;
( ~ (g . (x ~)) = g . (x ~) & ~ (g . (y ~)) = g . (y ~) ) ;
hence for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b2 <= b1 ) by A1, A9, Th1; :: thesis: verum
end;