let S, T be complete LATTICE; :: thesis: for f being monotone Function of S,T
for x being Element of S holds f . x = sup (f .: (downarrow x))
let f be monotone Function of S,T; :: thesis: for x being Element of S holds f . x = sup (f .: (downarrow x))
let x be Element of S; :: thesis: f . x = sup (f .: (downarrow x))
A1: for b being Element of T st b is_>=_than f .: (downarrow x) holds
f . x <= b

proof

let b be Element of T; :: thesis: ( b is_>=_than f .: (downarrow x) implies f . x <= b )
x <= x ;
then ( dom f = the carrier of S & x in downarrow x ) by FUNCT_2:def 1, WAYBEL_0:17;
then A2: f . x in f .: (downarrow x) by FUNCT_1:def 6;
assume b is_>=_than f .: (downarrow x) ; :: thesis: f . x <= b
hence f . x <= b by A2; :: thesis: verum

end;

( ex_sup_of downarrow x,S & sup (downarrow x) = x ) by WAYBEL_0:34;
then downarrow x is_<=_than x by YELLOW_0:30;
then f .: (downarrow x) is_<=_than f . x by YELLOW_2:14;
hence f . x = sup (f .: (downarrow x)) by A1, YELLOW_0:30; :: thesis: verum