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