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