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: ex_sup_of downarrow x,S by WAYBEL_0:34;
sup (downarrow x) = x by WAYBEL_0:34;
then downarrow x is_<=_than x by A1, YELLOW_0:30;
then A2: f .: (downarrow x) is_<=_than f . x by YELLOW_2:16;
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 )
assume A3: b is_>=_than f .: (downarrow x) ; :: thesis: f . x <= b
A4: dom f = the carrier of S by FUNCT_2:def 1;
x <= x ;
then x in downarrow x by WAYBEL_0:17;
then f . x in f .: (downarrow x) by A4, FUNCT_1:def 12;
hence f . x <= b by A3, LATTICE3:def 9; :: thesis: verum

end;

hence f . x = sup (f .: (downarrow x)) by A2, YELLOW_0:30; :: thesis: verum