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 holds f . x = "\/" { (f . w) where w is Element of : w << x } ,T ) holds
for x being Element of
for y being Element of holds
( y << f . x iff ex w being Element of 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 holds f . x = "\/" { (f . w) where w is Element of : w << x } ,T ) holds
for x being Element of
for y being Element of holds
( y << f . x iff ex w being Element of st
( w << x & y << f . w ) )
let f be Function of S,T; :: thesis: ( ( for x being Element of holds f . x = "\/" { (f . w) where w is Element of : w << x } ,T ) implies for x being Element of
for y being Element of holds
( y << f . x iff ex w being Element of st
( w << x & y << f . w ) ) )
assume A1: for x being Element of holds f . x = "\/" { (f . w) where w is Element of : w << x } ,T ; :: thesis: for x being Element of
for y being Element of holds
( y << f . x iff ex w being Element of st
( w << x & y << f . w ) )
then A2: f is monotone by Th13;
let x be Element of ; :: thesis: for y being Element of holds
( y << f . x iff ex w being Element of st
( w << x & y << f . w ) )
let y be Element of ; :: thesis: ( y << f . x iff ex w being Element of st
( w << x & y << f . w ) )

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

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