let S be lower-bounded up-complete LATTICE; :: thesis: for T being lower-bounded continuous LATTICE
for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let T be lower-bounded continuous LATTICE; :: thesis: for f being Function of S,T st ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) holds
for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let f be Function of S,T; :: thesis: ( ( for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ) implies for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) ) )
assume A1: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) ; :: thesis: for x being Element of S
for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
then A2: f is monotone by Th13;
let x be Element of S; :: thesis: for y being Element of T holds
( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
let y be Element of T; :: thesis: ( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )

hereby :: thesis: ( ex w being Element of S st
( w << x & y << f . w ) implies y << f . x )

assume A3: y << f . x ; :: thesis: ex v being Element of S st
( v << x & y << f . v )
reconsider D = f .: (waybelow x) as non empty directed Subset of T by A1, Th13, YELLOW_2:15;
A4: f . x = "\/" ( { (f . w) where w is Element of S : w << x } ,T) by A1;
A5: the carrier of S c= dom f by FUNCT_2:def 1;
defpred S₁[ Element of S] means $1 << x;
deffunc H₁( Element of S) -> Element of S = $1;
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(A5);
then consider w being Element of T such that
A6: w in D and
A7: y << w by A3, A4, WAYBEL_4:53;
consider v being object such that
A8: v in the carrier of S and
A9: v in waybelow x and
A10: w = f . v by A6, FUNCT_2:64;
reconsider v = v as Element of S by A8;
take v = v; :: thesis: ( v << x & y << f . v )
thus ( v << x & y << f . v ) by A7, A9, A10, WAYBEL_3:7; :: thesis: verum

end;

given w being Element of S such that A11: w << x and
A12: y << f . w ; :: thesis: y << f . x
w <= x by A11, WAYBEL_3:1;
then f . w <= f . x by A2;
hence y << f . x by A12, WAYBEL_3:2; :: thesis: verum