let I be set ; :: thesis: for M being ManySortedSet of holds [0] I is V9() V29() MSSubsetFamily of M
let M be ManySortedSet of ; :: thesis: [0] I is V9() V29() MSSubsetFamily of M
[0] I c= bool M by PBOOLE:49;
hence [0] I is V9() V29() MSSubsetFamily of M by PBOOLE:def 23; :: thesis: verum