let S be LATTICE; :: thesis: for T being lower-bounded up-complete LATTICE

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

f is monotone

let T be lower-bounded up-complete LATTICE; :: thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

f is monotone

let f be Function of S,T; :: thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is monotone )

assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: 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 )

deffunc H_{1}( Element of S) -> Element of S = $1;

defpred S_{1}[ Element of S] means $1 << X;

defpred S_{2}[ Element of S] means $1 << Y;

assume X <= Y ; :: thesis: f . X <= f . Y

then A2: waybelow X c= waybelow Y by WAYBEL_3:12;

A3: f . X = "\/" ( { (f . w) where w is Element of S : w << X } ,T) by A1;

A4: the carrier of S c= dom f by FUNCT_2:def 1;

A5: f .: { H_{1}(w) where w is Element of S : S_{1}[w] } = { (f . H_{1}(w)) where w is Element of S : S_{1}[w] }
from WAYBEL17:sch 2(A4);

f .: { H_{1}(w) where w is Element of S : S_{2}[w] } = { (f . H_{1}(w)) where w is Element of S : S_{2}[w] }
from WAYBEL17:sch 2(A4);

then A6: f . Y = "\/" ((f .: (waybelow Y)),T) by A1;

A7: ex_sup_of f .: (waybelow X),T by YELLOW_0:17;

ex_sup_of f .: (waybelow Y),T by YELLOW_0:17;

hence f . X <= f . Y by A2, A3, A5, A6, A7, RELAT_1:123, YELLOW_0:34; :: thesis: verum

for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

f is monotone

let T be lower-bounded up-complete LATTICE; :: thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds

f is monotone

let f be Function of S,T; :: thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies f is monotone )

assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: 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 )

deffunc H

defpred S

defpred S

assume X <= Y ; :: thesis: f . X <= f . Y

then A2: waybelow X c= waybelow Y by WAYBEL_3:12;

A3: f . X = "\/" ( { (f . w) where w is Element of S : w << X } ,T) by A1;

A4: the carrier of S c= dom f by FUNCT_2:def 1;

A5: f .: { H

f .: { H

then A6: f . Y = "\/" ((f .: (waybelow Y)),T) by A1;

A7: ex_sup_of f .: (waybelow X),T by YELLOW_0:17;

ex_sup_of f .: (waybelow Y),T by YELLOW_0:17;

hence f . X <= f . Y by A2, A3, A5, A6, A7, RELAT_1:123, YELLOW_0:34; :: thesis: verum