for a being Element of Z_2 holds
( a = 0 or a = 1 ) by CARD_1:50, TARSKI:def 2;