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