deffunc H₁( set ) -> set = bool (A . $1);
thus ex X being ManySortedSet of I st
for i being set st i in I holds
X . i = H₁(i) from PBOOLE:sch 4(); :: thesis: verum