deffunc H₁( set , Element of the carrier of S * ) -> Element of K19(K20(((len c₂) -tuples_on BOOLEAN),BOOLEAN)) = ((len c₂) -tuples_on BOOLEAN) --> FALSE;
A1: for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H₁(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN ;
consider A being strict MSAlgebra over S such that
A2: ( the Sorts of A = the carrier of S --> BOOLEAN & ( for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
the Charact of A . g = H₁(g,p) ) ) from CIRCCOMB:sch 2(A1);
take A ; :: thesis: A is Boolean
let v be Vertex of S; :: according to CIRCCOMB:def 14 :: thesis: the Sorts of A . v = BOOLEAN
thus the Sorts of A . v = BOOLEAN by A2; :: thesis: verum