per cases ( not SF is empty or SF is empty ) ;

suppose A1: not SF is empty ; :: thesis: |:SF:| is MSSubsetFamily of M

|:SF:| is ManySortedSubset of bool M

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in I or |:SF:| . i c= (bool M) . i )
assume A2: i in I ; :: thesis: |:SF:| . i c= (bool M) . i
then A3: |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A1, Th14;
thus |:SF:| . i c= (bool M) . i :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in |:SF:| . i or x in (bool M) . i )
assume x in |:SF:| . i ; :: thesis: x in (bool M) . i
then consider a being Element of Bool M such that
A4: x = a . i and
a in SF by A3;
a c= M by PBOOLE:def 18;
then a . i c= M . i by A2;
then x in bool (M . i) by A4;
hence x in (bool M) . i by A2, MBOOLEAN:def 1; :: thesis: verum

end;

end;

hence |:SF:| is MSSubsetFamily of M ; :: thesis: verum

end;

suppose SF is empty ; :: thesis: |:SF:| is MSSubsetFamily of M

then |:SF:| = EmptyMS I ;
hence |:SF:| is MSSubsetFamily of M by MSSUBFAM:31; :: thesis: verum

end;

end;