let I be set ; :: thesis: for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF holds
A is ManySortedSubset of M
let A, M be ManySortedSet of I; :: 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 )
A1: SF c= bool M by PBOOLE:def 18;
assume A in SF ; :: thesis: A is ManySortedSubset of M
then A in bool M by A1, PBOOLE:9;
then A c= M by MBOOLEAN:18;
hence A is ManySortedSubset of M by PBOOLE:def 18; :: thesis: verum