deffunc H₁( Element of bool X) -> Element of ExtREAL = inf (Svc (M,$1));
thus ex G being Function of (bool X),ExtREAL st
for A being Subset of X holds G . A = H₁(A) from FUNCT_2:sch 4(); :: thesis: verum