let I be set ; :: thesis:
let A, M be ManySortedSet of I; :: thesis:
let SF be V8() MSSubsetFamily of M; :: thesis:
assume that
A1: A in M and
A2: for B being ManySortedSet of I st B in SF holds
A in B ; :: thesis:
let i be object ; :: according to PBOOLE:def 1 :: thesis:
consider T being ManySortedSet of I such that
A3: T in SF by PBOOLE:134;
assume A4: i in I ; :: thesis:
then consider Q being Subset-Family of (M . i) such that
A5: Q = SF . i and
A6: (meet SF) . i = Intersect Q by Def1;
A7: for B9 being set st B9 in Q holds
A . i in B9

let B9 be set ; :: thesis:
assume A8: B9 in Q ; :: thesis:
dom (T +* (i .--> B9)) = I by A4, PZFMISC1:1;
then reconsider K = T +* (i .--> B9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A9: dom (i .--> B9) = {i} ;
i in {i} by TARSKI:def 1;
then A10: K . i = (i .--> B9) . i by A9, FUNCT_4:13
.= B9 by FUNCOP_1:72 ;
K in SF

let q be object ; :: according to PBOOLE:def 1 :: thesis:
assume A11: q in I ; :: thesis:

hence K . q in SF . q by A5, A8, A10; :: thesis:

end;

end;

then A in K by A2;
hence A . i in B9 by A4, A10; :: thesis:

end;

A . i in M . i by A1, A4;
hence A . i in (meet SF) . i by A6, A7, SETFAM_1:43; :: thesis: