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 by WAYBEL_0:def 9; :: thesis: verum