theorem ThB1: :: ABSRED_0:89

for s being set holds
( s is Element of ARS_02 iff ( s = 0 or s = 1 or s = 2 ) )