theorem :: ABSRED_0:90

for m, n being Element of ARS_02 holds
( m ==> n iff m = 0 )