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