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
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 20;
hence y in f " P by FUNCT_2:38; :: thesis: verum
end;
hence f " P is upper ; :: thesis: verum