deffunc H₁( Subset of T) -> Element of bool the carrier of T = Cl $1;
set X = the carrier of T;
ex g being Function of (bool the carrier of T),(bool the carrier of T) st
for x being Element of bool the carrier of T holds g . x = H₁(x) from FUNCT_2:sch 4();
then consider g being Function of (bool the carrier of T),(bool the carrier of T) such that
A1: for x being Element of bool the carrier of T holds g . x = H₁(x) ;
take g ; :: thesis: for X being Subset of T holds g . X = Cl X
let x be Subset of the carrier of T; :: thesis: g . x = Cl x
thus g . x = Cl x by A1; :: thesis: verum