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

proof

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;

hence f " P is lower ; :: thesis: verum