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 )
assume A1: f is monotone ; :: thesis: f .: X is directed
set Y = f .: X;
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 A2: ( y1 in f .: X & y2 in f .: X ) ; :: thesis: ex z being Element of T st
( z in f .: X & y1 <= z & y2 <= z )
then consider x1 being set such that
x1 in dom f and
A3: x1 in X and
A4: y1 = f . x1 by FUNCT_1:def 12;
consider x2 being set such that
x2 in dom f and
A5: x2 in X and
A6: y2 = f . x2 by A2, FUNCT_1:def 12;
reconsider x1 = x1, x2 = x2 as Element of S by A3, A5;
consider z being Element of S such that
A7: ( z in X & x1 <= z & x2 <= z ) by A3, A5, 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 A7, FUNCT_2:43; :: thesis: ( y1 <= f . z & y2 <= f . z )
thus ( y1 <= f . z & y2 <= f . z ) by A1, A4, A6, A7, ORDERS_3:def 5; :: thesis: verum

end;

hence f .: X is directed by WAYBEL_0:def 1; :: thesis: verum