M # is non-empty

proof

let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in I * or not (M #) . i is empty )
assume i in I * ; :: thesis: not (M #) . i is empty
then reconsider f = i as Element of I * ;
product (M * f) <> {} ;
hence not (M #) . i is empty by Def5; :: thesis: verum

end;

hence M # is non-empty ; :: thesis: verum