theorem :: ABSRED_0:90
for m, n being Element of ARS_02 holds
( m ==> n iff m = 0 )