:: deftheorem Def1 defines inv1 GFACIRC1:def 1 :
for b₁ being Function of (1 -tuples_on BOOLEAN),BOOLEAN holds
( b₁ = inv1 iff for x being Element of BOOLEAN holds b₁ . <*x*> = 'not' x );