let i be set ; :: according to PBOOLE:def 5,PBOOLE:def 23 :: thesis: ( not i in I or (meet SF) . i c= M . i )
assume i in I ; :: thesis: (meet SF) . i c= M . i
then consider Q being Subset-Family of (M . i) such that
A1: ( Q = SF . i & (meet SF) . i = Intersect Q ) by Def2;
thus (meet SF) . i c= M . i by A1; :: thesis: verum