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
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 S1[ Element of S] means ( \$1 <= X & \$1 is compact );
defpred S2[ Element of S] means ( \$1 <= Y & \$1 is compact );
deffunc H1( Element of S) -> Element of S = \$1;
f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from then A6: f . X = "\/" ((f .: ()),T) by ;
f .: { H1(w) where w is Element of S : S2[w] } = { (f . H1(w)) where w is Element of S : S2[w] } from then A7: f . Y = "\/" ((f .: ()),T) by ;
A8: 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
end;