let I be set ; :: thesis: for A, M being ManySortedSet of
for SF being MSSubsetFamily of M st A in SF holds
A is ManySortedSubset of M
let A, M be ManySortedSet of ; :: thesis: for SF being MSSubsetFamily of M st A in SF holds
A is ManySortedSubset of M
let SF be MSSubsetFamily of M; :: thesis: ( A in SF implies A is ManySortedSubset of M )
assume A1: A in SF ; :: thesis: A is ManySortedSubset of M
SF c= bool M by PBOOLE:def 23;
then A in bool M by A1, PBOOLE:9;
then A c= M by MBOOLEAN:19;
hence A is ManySortedSubset of M by PBOOLE:def 23; :: thesis: verum