deffunc H_{1}( 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_{1}(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_{1}(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

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

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

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