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 A2, YELLOW_2:17;
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 & y << w ) by A3, A4, WAYBEL_4:54;
consider v being set such that
A7: ( v in the carrier of S & v in waybelow x & w = f . v ) by A6, FUNCT_2:115;
reconsider v = v as Element of S by A7;
take v = v; :: thesis: ( v << x & y << f . v )
thus ( v << x & y << f . v ) by A6, A7, WAYBEL_3:7; :: thesis: verum

end;

given w being Element of S such that A8: ( w << x & y << f . w ) ; :: thesis: y << f . x
w <= x by A8, WAYBEL_3:1;
then f . w <= f . x by A2, WAYBEL_1:def 2;
hence y << f . x by A8, WAYBEL_3:2; :: thesis: verum