let S be LATTICE; :: thesis: for T being 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 & w is compact ) } ,T) ) holds

f is monotone

let T be 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 & w is compact ) } ,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 & w is compact ) } ,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 & w is compact ) } ,T) ; :: thesis: f is monotone

thus f is monotone :: 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 & w is compact ) } ,T) ) holds

f is monotone

let T be 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 & w is compact ) } ,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 & w is compact ) } ,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 & w is compact ) } ,T) ; :: thesis: f is monotone

thus f is monotone :: thesis: verum

proof

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 A2: compactbelow X c= compactbelow Y by WAYBEL13:1;

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

A4: f . Y = "\/" ( { (f . w) where w is Element of S : ( w <= Y & w is compact ) } ,T) by A1;

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

defpred S_{1}[ Element of S] means ( $1 <= X & $1 is compact );

defpred S_{2}[ Element of S] means ( $1 <= Y & $1 is compact );

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

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(A5);

then A6: f . X = "\/" ((f .: (compactbelow X)),T) by A3, WAYBEL_8:def 2;

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(A5);

then A7: f . Y = "\/" ((f .: (compactbelow Y)),T) by A4, WAYBEL_8:def 2;

A8: ex_sup_of f .: (compactbelow X),T by YELLOW_0:17;

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

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

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

then A2: compactbelow X c= compactbelow Y by WAYBEL13:1;

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

A4: f . Y = "\/" ( { (f . w) where w is Element of S : ( w <= Y & w is compact ) } ,T) by A1;

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

defpred S

defpred S

deffunc H

f .: { H

then A6: f . X = "\/" ((f .: (compactbelow X)),T) by A3, WAYBEL_8:def 2;

f .: { H

then A7: f . Y = "\/" ((f .: (compactbelow Y)),T) by A4, WAYBEL_8:def 2;

A8: ex_sup_of f .: (compactbelow X),T by YELLOW_0:17;

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

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