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 ) )

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

thus
( g is antitone implies f is monotone )
:: thesis: ( f is antitone iff g is monotone )
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_{1}, b_{2} being Element of the carrier of (T ~) holds

( not b_{1} = g . x or not b_{2} = g . y or b_{2} <= b_{1} ) )

assume x <= y ; :: thesis: for b_{1}, b_{2} being Element of the carrier of (T ~) holds

( not b_{1} = g . x or not b_{2} = g . y or b_{2} <= b_{1} )

then A3: f . x <= f . y by A2;

( (f . x) ~ = f . x & (f . y) ~ = f . y ) ;

hence for b_{1}, b_{2} being Element of the carrier of (T ~) holds

( not b_{1} = g . x or not b_{2} = g . y or b_{2} <= b_{1} )
by A1, A3, LATTICE3:9; :: thesis: verum

end;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

( not b

assume x <= y ; :: thesis: for b

( not b

then A3: f . x <= f . y by A2;

( (f . x) ~ = f . x & (f . y) ~ = f . y ) ;

hence for b

( not b

proof

thus
( f is antitone implies g is monotone )
:: thesis: ( g is monotone implies f is antitone )
assume A4:
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 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;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 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

proof

thus
( g is monotone implies f is antitone )
:: thesis: verum
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 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 A7: f . y <= f . x by A6;

( (f . x) ~ = f . x & (f . y) ~ = f . y ) ;

hence g . x <= g . y by A1, A7, LATTICE3:9; :: thesis: verum

end;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 A7: f . y <= f . x by A6;

( (f . x) ~ = f . x & (f . y) ~ = f . y ) ;

hence g . x <= g . y by A1, A7, LATTICE3:9; :: thesis: verum

proof

assume A8:
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_{1}, b_{2} being Element of the carrier of T holds

( not b_{1} = f . x or not b_{2} = f . y or b_{2} <= b_{1} ) )

assume x <= y ; :: thesis: for b_{1}, b_{2} being Element of the carrier of T holds

( not b_{1} = f . x or not b_{2} = f . y or b_{2} <= b_{1} )

then A9: g . y >= g . x by A8;

( ~ (g . x) = g . x & ~ (g . y) = g . y ) ;

hence for b_{1}, b_{2} being Element of the carrier of T holds

( not b_{1} = f . x or not b_{2} = f . y or b_{2} <= b_{1} )
by A1, A9, Th1; :: thesis: verum

end;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

( not b

assume x <= y ; :: thesis: for b

( not b

then A9: g . y >= g . x by A8;

( ~ (g . x) = g . x & ~ (g . y) = g . y ) ;

hence for b

( not b