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

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