SF c= bool M by PBOOLE:def 18;
then SF . i c= (bool M) . i ;
hence SF . i is Subset-Family of (M . i) by MBOOLEAN:def 1; :: thesis: verum