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