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 by WAYBEL_0:def 10;
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_0:def 5; :: 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₁ ) )
( 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; :: thesis: verum