deffunc H₁( set ) -> Subset of X = F_LABEL $1,X;
A1: for x being set st x in S holds
H₁(x) in bool X ;
consider IT being Function of S,(bool X) such that
A2: for x being set st x in S holds
IT . x = H₁(x) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: for x being set st x in S holds
IT . x = F_LABEL x,X
thus for x being set st x in S holds
IT . x = F_LABEL x,X by A2; :: thesis: verum