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

assume N is antitone ; :: thesis: for i, j being Element of N st i <= j holds
N . i >= N . j
then A1: netmap (N,T) is antitone ;
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 antitone
let i, j be Element of N; :: according to WAYBEL_0:def 5,WAYBEL_0:def 10 :: thesis: ( not i <= j or for b₁, b₂ being Element of the carrier of T holds
( not b₁ = (netmap (N,T)) . i or not b₂ = (netmap (N,T)) . j or b₂ <= b₁ ) )
A3: N . i = (netmap (N,T)) . i ;
N . j = (netmap (N,T)) . j ;
hence ( not i <= j or for b₁, b₂ being Element of the carrier of T holds
( not b₁ = (netmap (N,T)) . i or not b₂ = (netmap (N,T)) . j or b₂ <= b₁ ) ) by A2, A3; :: thesis: verum