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

consider g being map of R such that

A1: for x being Element of bool the carrier of R holds g . x = H

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

hence
g . x = { u where u is Element of R : f . u meets x }
by A2, SUBSET_1:def 8; :: thesis: verum
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;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