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 H1( Element of S) -> Element of S = \$1;
defpred S1[ Element of S] means \$1 << X;
defpred S2[ 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 .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from f .: { H1(w) where w is Element of S : S2[w] } = { (f . H1(w)) where w is Element of S : S2[w] } from then A6: f . Y = "\/" ((f .: ()),T) by A1;
A7: ex_sup_of f .: (),T by YELLOW_0:17;
ex_sup_of f .: (),T by YELLOW_0:17;
hence f . X <= f . Y by ; :: thesis: verum