let S, T be non empty RelStr ; :: thesis: for f being Function of S,T
for g being Function of S,(T opp ) st f = g holds
( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) )
let f be Function of S,T; :: thesis: for g being Function of S,(T opp ) st f = g holds
( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) )
let g be Function of S,(T ~ ); :: thesis: ( f = g implies ( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) ) )
assume A1: f = g ; :: thesis: ( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) )
thus ( f is monotone implies g is antitone ) :: thesis: ( ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone 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 antitone
let x, y be Element of S; :: according to WAYBEL_0:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of (T ~ ) holds
( not b₁ = g . x or not b₂ = g . y or b₂ <= b₁ ) )
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of (T ~ ) holds
( not b₁ = g . x or not b₂ = g . y or b₂ <= b₁ )
then ( f . x <= f . y & (f . x) ~ = f . x & (f . y) ~ = f . y ) by A2;
hence for b₁, b₂ being Element of the carrier of (T ~ ) holds
( not b₁ = g . x or not b₂ = g . y or b₂ <= b₁ ) by A1, LATTICE3:9; :: thesis: verum

end;

thus ( g is antitone implies f is monotone ) :: thesis: ( f is antitone iff g is monotone )

proof

assume A3: for x, y being Element of S 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 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 ( g . y <= g . x & ~ (g . x) = g . x & ~ (g . y) = g . y ) by A3;
hence f . x <= f . y by A1, Th1; :: thesis: verum

end;

thus ( f is antitone implies g is monotone ) :: thesis: ( g is monotone implies f is antitone )

proof

assume A4: 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 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 ( f . y <= f . x & (f . x) ~ = f . x & (f . y) ~ = f . y ) by A4;
hence g . x <= g . y by A1, LATTICE3:9; :: thesis: verum

end;

thus ( g is monotone implies f is antitone ) :: thesis: verum

proof

assume A5: for x, y being Element of S st x <= y holds
g . x <= g . y ; :: according to WAYBEL_1:def 2 :: thesis: f is antitone
let x, y be Element of S; :: according to WAYBEL_0:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₂ <= b₁ ) )
assume x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₂ <= b₁ )
then ( g . y >= g . x & ~ (g . x) = g . x & ~ (g . y) = g . y ) by A5;
hence for b₁, b₂ being Element of the carrier of T holds
( not b₁ = f . x or not b₂ = f . y or b₂ <= b₁ ) by A1, Th1; :: thesis: verum

end;