let i, j be Element of ARS_01; :: thesis: ( i ==> j iff i = 0 )
the reduction of ARS_01 = [:{0},{0,1}:] by Def18;
then ( i ==> j iff ( i in {0} & j in {0,1} ) ) by ZFMISC_1:87;
then ( i ==> j iff ( i = 0 & ( j = 0 or j = 1 ) ) ) by TARSKI:def 1, TARSKI:def 2;
hence ( i ==> j iff i = 0 ) by ThA1; :: thesis: verum