deffunc H₂( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) -> Element of BOOLEAN = (('not' $1) '&' ('not' $2)) '&' $3;
thus ex t being Function of (3 -tuples_on BOOLEAN),BOOLEAN st
for x, y, z being Element of BOOLEAN holds t . <*x,y,z*> = H₂(x,y,z) from FACIRC_1:sch 4(); :: thesis: verum