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