hereby :: thesis: ( ( for i, j being Element of N st i <= j holds
N . i <= N . j ) implies N is monotone )

assume N is monotone ; :: thesis: for i, j being Element of N st i <= j holds
N . i <= N . j
then A1: netmap (N,R) is monotone ;
let i, j be Element of N; :: thesis: ( i <= j implies N . i <= N . j )
assume i <= j ; :: thesis: N . i <= N . j
hence N . i <= N . j by A1; :: thesis: verum

end;

assume A2: for i, j being Element of N st i <= j holds
N . i <= N . j ; :: thesis: N is monotone
netmap (N,R) is monotone

proof

let x, y be Element of N; :: according to WAYBEL_1:def 2 :: thesis: ( not x <= y or (netmap (N,R)) . x <= (netmap (N,R)) . y )
A3: (netmap (N,R)) . x = N . x ;
A4: (netmap (N,R)) . y = N . y ;
assume x <= y ; :: thesis: (netmap (N,R)) . x <= (netmap (N,R)) . y
hence (netmap (N,R)) . x <= (netmap (N,R)) . y by A2, A3, A4; :: thesis: verum

end;

hence N is monotone ; :: thesis: verum