let i be set ; :: 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 Def2;
hence (meet SF) . i c= M . i ; :: thesis: verum