theorem :: ABSRED_0:88

for i, j being Element of ARS_01 holds
( i ==> j iff i = 0 )