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

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

f " P is upper

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

f " P is upper

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

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

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

y in f " P

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

f " P is upper

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

f " P is upper

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

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

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

y in f " P

proof

hence
f " P is upper
; :: 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 20;

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 20;

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