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;
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 ;
hence f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: thesis: verum