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