let I be set ; :: thesis: for i being object
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st i in I holds
SF . i is Subset-Family of (M . i)
let i be object ; :: thesis: for M being ManySortedSet of I
for SF being MSSubsetFamily of M st i in I holds
SF . i is Subset-Family of (M . i)
let M be ManySortedSet of I; :: thesis: for SF being MSSubsetFamily of M st i in I holds
SF . i is Subset-Family of (M . i)
let SF be MSSubsetFamily of M; :: thesis: ( i in I implies SF . i is Subset-Family of (M . i) )
assume A1: i in I ; :: thesis: SF . i is Subset-Family of (M . i)
SF c= bool M by PBOOLE:def 18;
then SF . i c= (bool M) . i by A1;
hence SF . i is Subset-Family of (M . i) by A1, MBOOLEAN:def 1; :: thesis: verum