deffunc H₁( Subset of T) -> Element of bool the carrier of T = Int $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
A4: 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 = Int X
let x be Subset of the carrier of T; :: thesis: g . x = Int x
thus g . x = Int x by A4; :: thesis: verum