let S, T be non empty reflexive RelStr ; :: thesis: for f being Function of S,T

for P being lower Subset of T st f is monotone holds

f " P is lower

let f be Function of S,T; :: thesis: for P being lower Subset of T st f is monotone holds

f " P is lower

let P be lower Subset of T; :: thesis: ( f is monotone implies f " P is lower )

assume A1: f is monotone ; :: thesis: f " P is lower

for x, y being Element of S st x in f " P & y <= x holds

y in f " P

for P being lower Subset of T st f is monotone holds

f " P is lower

let f be Function of S,T; :: thesis: for P being lower Subset of T st f is monotone holds

f " P is lower

let P be lower Subset of T; :: thesis: ( f is monotone implies f " P is lower )

assume A1: f is monotone ; :: thesis: f " P is lower

for x, y being Element of S st x in f " P & y <= x holds

y in f " P

proof

hence
f " P is lower
; :: thesis: verum
let x, y be Element of S; :: thesis: ( x in f " P & y <= x implies y in f " P )

assume that

A2: x in f " P and

A3: y <= x ; :: thesis: y in f " P

A4: f . y <= f . x by A1, A3;

reconsider fy = f . y, fx = f . x as Element of T ;

fx in P by A2, FUNCT_2:38;

then fy in P by A4, WAYBEL_0:def 19;

hence y in f " P by FUNCT_2:38; :: thesis: verum

end;assume that

A2: x in f " P and

A3: y <= x ; :: thesis: y in f " P

A4: f . y <= f . x by A1, A3;

reconsider fy = f . y, fx = f . x as Element of T ;

fx in P by A2, FUNCT_2:38;

then fy in P by A4, WAYBEL_0:def 19;

hence y in f " P by FUNCT_2:38; :: thesis: verum