let S, T be lower-bounded continuous LATTICE; :: thesis: for f being Function of S,T st f is directed-sups-preserving holds

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)

let f be Function of S,T; :: thesis: ( f is directed-sups-preserving implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )

assume A1: f is directed-sups-preserving ; :: 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)

defpred S_{1}[ Element of S] means $1 << x;

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

A2: f preserves_sup_of waybelow x by A1;

A3: ex_sup_of waybelow x,S by YELLOW_0:17;

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

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

f . x = f . (sup (waybelow x)) by WAYBEL_3:def 5

.= "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A2, A3, A5 ;

hence f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: thesis: verum

for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T)

let f be Function of S,T; :: thesis: ( f is directed-sups-preserving implies for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) )

assume A1: f is directed-sups-preserving ; :: 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)

defpred S

deffunc H

A2: f preserves_sup_of waybelow x by A1;

A3: ex_sup_of waybelow x,S by YELLOW_0:17;

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

A5: f .: { H

f . x = f . (sup (waybelow x)) by WAYBEL_3:def 5

.= "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A2, A3, A5 ;

hence f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: thesis: verum