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 ) )

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

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 )

given w being Element of S such that A11:
w << x
and ( 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_{1}[ Element of S] means $1 << x;

deffunc H_{1}( Element of S) -> Element of S = $1;

f .: { H_{1}(w) where w is Element of S : S_{1}[w] } = { (f . H_{1}(w)) where w is Element of S : S_{1}[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;( 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

deffunc H

f .: { H

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

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