:: deftheorem Def19 defines ARS_02 ABSRED_0:def 10 :
for b₁ being strict ARS holds
( b₁ = ARS_02 iff ( the carrier of b₁ = {0,1,2} & the reduction of b₁ = [:{0},{0,1,2}:] ) );