let m, n be Element of ARS_02; :: thesis: ( m ==> n iff m = 0 )
the reduction of ARS_02 = [:{0},{0,1,2}:] by Def19;
then ( m ==> n iff ( m in {0} & n in {0,1,2} ) ) by ZFMISC_1:87;
then ( m ==> n iff ( m = 0 & ( n = 0 or n = 1 or n = 2 ) ) ) by TARSKI:def 1, ENUMSET1:def 1;
hence ( m ==> n iff m = 0 ) by ThB1; :: thesis: verum