let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in I or (meet SF) . i c= M . i )
assume i in I ; :: thesis: (meet SF) . i c= M . i
then ex Q being Subset-Family of (M . i) st
( Q = SF . i & (meet SF) . i = Intersect Q ) by Def1;
hence (meet SF) . i c= M . i ; :: thesis: verum