let I be set ; :: thesis: for M, A being ManySortedSet of
for SF being MSSubsetFamily of M st A in SF holds
meet SF c= A
let M, A be ManySortedSet of ; :: thesis: for SF being MSSubsetFamily of M st A in SF holds
meet SF c= A
let SF be MSSubsetFamily of M; :: thesis: ( A in SF implies meet SF c= A )
assume A1: A in SF ; :: thesis: meet SF c= A
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (meet SF) . i c= A . i )
assume A2: i in I ; :: thesis: (meet SF) . i c= A . i
then consider Q being Subset-Family of (M . i) such that
A3: Q = SF . i and
A4: (meet SF) . i = Intersect Q by Def2;
A5: A . i in SF . i by A1, A2, PBOOLE:def 4;
then Intersect Q = meet Q by A3, SETFAM_1:def 10;
hence (meet SF) . i c= A . i by A3, A4, A5, SETFAM_1:4; :: thesis: verum