theorem :: BSPACE:8

for x being Element of Z_2 holds
( x = 0. Z_2 iff x <> 1. Z_2 ) by Th5, Th6, CARD_1:50, TARSKI:def 2;