let S, T be non empty RelStr ; :: thesis: for f being Function of S,T
for X being directed Subset of S st f is monotone holds
f .: X is directed
let f be Function of S,T; :: thesis: for X being directed Subset of S st f is monotone holds
f .: X is directed
let X be directed Subset of S; :: thesis: ( f is monotone implies f .: X is directed )
set Y = f .: X;
assume A1: f is monotone ; :: thesis: f .: X is directed
for y1, y2 being Element of T st y1 in f .: X & y2 in f .: X holds
ex z being Element of T st
( z in f .: X & y1 <= z & y2 <= z )

proof

let y1, y2 be Element of T; :: thesis: ( y1 in f .: X & y2 in f .: X implies ex z being Element of T st
( z in f .: X & y1 <= z & y2 <= z ) )
assume that
A2: y1 in f .: X and
A3: y2 in f .: X ; :: thesis: ex z being Element of T st
( z in f .: X & y1 <= z & y2 <= z )
consider x1 being object such that
x1 in dom f and
A4: x1 in X and
A5: y1 = f . x1 by A2, FUNCT_1:def 6;
consider x2 being object such that
x2 in dom f and
A6: x2 in X and
A7: y2 = f . x2 by A3, FUNCT_1:def 6;
reconsider x1 = x1, x2 = x2 as Element of S by A4, A6;
consider z being Element of S such that
A8: z in X and
A9: ( x1 <= z & x2 <= z ) by A4, A6, WAYBEL_0:def 1;
take f . z ; :: thesis: ( f . z in f .: X & y1 <= f . z & y2 <= f . z )
thus f . z in f .: X by A8, FUNCT_2:35; :: thesis: ( y1 <= f . z & y2 <= f . z )
thus ( y1 <= f . z & y2 <= f . z ) by A1, A5, A7, A9; :: thesis: verum

end;

hence f .: X is directed ; :: thesis: verum