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