deffunc H₁( Subset of R) -> Element of bool the carrier of R = In ( { u where u is Element of R : f . u meets $1 } ,(bool the carrier of R));
consider g being map of R such that
A1: for x being Element of bool the carrier of R holds g . x = H₁(x) from FUNCT_2:sch 4();
take g ; :: thesis: for x being Subset of R holds g . x = { u where u is Element of R : f . u meets x }
let x be Subset of R; :: thesis: g . x = { u where u is Element of R : f . u meets x }
A2: g . x = In ( { u where u is Element of R : f . u meets x } ,(bool the carrier of R)) by A1;
{ u where u is Element of R : f . u meets x } c= the carrier of R

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { u where u is Element of R : f . u meets x } or y in the carrier of R )
assume y in { u where u is Element of R : f . u meets x } ; :: thesis: y in the carrier of R
then consider u being Element of R such that
A3: ( y = u & f . u meets x ) ;
thus y in the carrier of R by A3; :: thesis: verum

end;

hence g . x = { u where u is Element of R : f . u meets x } by A2, SUBSET_1:def 8; :: thesis: verum