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