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 b1, b2 being Element of the carrier of T holds
( not b1 = (netmap (N,T)) . i or not b2 = (netmap (N,T)) . j or b2 <= b1 ) )
A3: N . i = (netmap (N,T)) . i ;
N . j = (netmap (N,T)) . j ;
hence ( not i <= j or for b1, b2 being Element of the carrier of T holds
( not b1 = (netmap (N,T)) . i or not b2 = (netmap (N,T)) . j or b2 <= b1 ) ) by A2, A3; :: thesis: verum