set M = the Sorts of D;
deffunc H₁( Element of Bool the Sorts of D) -> Element of Bool the Sorts of D = Cl $1;
consider f being Function of (Bool the Sorts of D),(Bool the Sorts of D) such that
A1: for x being Element of Bool the Sorts of D holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider f = f as SetOp of the Sorts of D ;
reconsider f = f as ClosureOperator of the Sorts of D by A1, Th40;
take f ; :: thesis: for x being Element of Bool the Sorts of D holds f . x = Cl x
thus for x being Element of Bool the Sorts of D holds f . x = Cl x by A1; :: thesis: verum