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₁[ Element of S] means $1 << x;
deffunc H₁( Element of S) -> Element of S = $1;
A2: f preserves_sup_of waybelow x by A1, WAYBEL_0:def 37;
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₁(w) where w is Element of S : S₁[w] } = { (f . H₁(w)) where w is Element of S : S₁[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, WAYBEL_0:def 31 ;
hence f . x = "\/" { (f . w) where w is Element of S : w << x } ,T ; :: thesis: verum