set N = Net-Str (S,f);
netmap ((Net-Str (S,f)),R) is monotone

proof

let x, y be Element of (Net-Str (S,f)); :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y )
A1: (netmap ((Net-Str (S,f)),R)) . x = (Net-Str (S,f)) . x ;
A2: (netmap ((Net-Str (S,f)),R)) . y = (Net-Str (S,f)) . y ;
assume x <= y ; :: thesis: (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y
hence (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y by A1, A2, Def10; :: thesis: verum

end;

hence Net-Str (S,f) is monotone ; :: thesis: verum