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₁( Element of S) -> Element of S = $1;
defpred S₁[ Element of S] means $1 << X;
defpred S₂[ 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₁(w) where w is Element of S : S₁[w] } = { (f . H₁(w)) where w is Element of S : S₁[w] } from WAYBEL17:sch 2(A4);
f .: { H₁(w) where w is Element of S : S₂[w] } = { (f . H₁(w)) where w is Element of S : S₂[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