deffunc H₁( Element of BOOLEAN ) -> Element of BOOLEAN = 'not' $1;
thus ex t being Function of 1 -tuples_on BOOLEAN , BOOLEAN st
for x being Element of BOOLEAN holds t . <*x*> = H₁(x) from GFACIRC1:sch 1(); :: thesis: verum