theorem ThA1: :: ABSRED_0:87

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