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

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