for X, x being set holds
( X @ x = 0. Z_2 iff not x in X ) by Def3;