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));
WAYBEL_1:def 2 ( 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
;
(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;
verum
end;
hence
Net-Str (S,f) is monotone
; verum