let s be set ; :: thesis: ( s is Element of ARS_02 iff ( s = 0 or s = 1 or s = 2 ) )
the carrier of ARS_02 = {0,1,2} by Def19;
hence ( s is Element of ARS_02 iff ( s = 0 or s = 1 or s = 2 ) ) by ENUMSET1:def 1; :: thesis: verum