deffunc H1( 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 = H1(x) from 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 ; :: thesis: verum