let S, T be lower-bounded complete LATTICE; :: thesis: for f being monotone Function of S,T
for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
let f be monotone 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)
let x be Element of S; :: thesis: f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T)
deffunc H₁( Element of S) -> Element of S = $1;
defpred S₁[ Element of S] means $1 <= x;
defpred S₂[ Element of S] means ex y1 being Element of S st
( $1 <= y1 & y1 in {x} );
A1: the carrier of S c= dom f by FUNCT_2:def 1;
A2: f .: { H₁(w) where w is Element of S : S₁[w] } = { (f . H₁(w)) where w is Element of S : S₁[w] } from WAYBEL24:sch 1(A1);
A3: for x2 being Element of S holds
( S₁[x2] iff S₂[x2] )

proof

let x2 be Element of S; :: thesis: ( S₁[x2] iff S₂[x2] )

hereby :: thesis: ( S₂[x2] implies S₁[x2] )

A4: x in {x} by TARSKI:def 1;
assume x2 <= x ; :: thesis: ex y1 being Element of S st
( x2 <= y1 & y1 in {x} )
hence ex y1 being Element of S st
( x2 <= y1 & y1 in {x} ) by A4; :: thesis: verum

end;

given y1 being Element of S such that A5: ( x2 <= y1 & y1 in {x} ) ; :: thesis: S₁[x2]
thus S₁[x2] by A5, TARSKI:def 1; :: thesis: verum

end;

{ H₁(w) where w is Element of S : S₁[w] } = { H₁(x1) where x1 is Element of S : S₂[x1] } from WAYBEL24:sch 2(A3);
then A6: downarrow x = { w where w is Element of S : w <= x } by WAYBEL_0:14;
sup (f .: (downarrow x)) = f . x by Th4
.= f . (sup (downarrow x)) by WAYBEL_0:34 ;
hence f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T) by A2, A6, WAYBEL_0:34; :: thesis: verum