let I be set ; :: thesis: for A, M being ManySortedSet of
for SF being V8() MSSubsetFamily of M st A in M & ( for B being ManySortedSet of st B in SF holds
A in B ) holds
A in meet SF
let A, M be ManySortedSet of ; :: thesis: for SF being V8() MSSubsetFamily of M st A in M & ( for B being ManySortedSet of st B in SF holds
A in B ) holds
A in meet SF
let SF be V8() MSSubsetFamily of M; :: thesis: ( A in M & ( for B being ManySortedSet of st B in SF holds
A in B ) implies A in meet SF )
assume that
A1: A in M and
A2: for B being ManySortedSet of st B in SF holds
A in B ; :: thesis: A in meet SF
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or A . i in (meet SF) . i )
assume A3: i in I ; :: thesis: A . i in (meet SF) . i
then consider Q being Subset-Family of (M . i) such that
A4: Q = SF . i and
A5: (meet SF) . i = Intersect Q by Def2;
A6: A . i in M . i by A1, A3, PBOOLE:def 4;
consider T being ManySortedSet of such that
A7: T in SF by PBOOLE:146;
for B' being set st B' in Q holds
A . i in B'

proof

let B' be set ; :: thesis: ( B' in Q implies A . i in B' )
assume A8: B' in Q ; :: thesis: A . i in B'
A9: dom (i .--> B') = {i} by FUNCOP_1:19;
dom (T +* (i .--> B')) = I by A3, PZFMISC1:1;
then reconsider K = T +* (i .--> B') as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
i in {i} by TARSKI:def 1;
then A10: K . i = (i .--> B') . i by A9, FUNCT_4:14
.= B' by FUNCOP_1:87 ;
K in SF

proof

let q be set ; :: according to PBOOLE:def 4 :: thesis: ( not q in I or K . q in SF . q )
assume A11: q in I ; :: thesis: K . q in SF . q

per cases ( q = i or q <> i ) ;

suppose q = i ; :: thesis: K . q in SF . q

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

end;

suppose q <> i ; :: thesis: K . q in SF . q

then not q in dom (i .--> B') by A9, TARSKI:def 1;
then K . q = T . q by FUNCT_4:12;
hence K . q in SF . q by A7, A11, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

then A in K by A2;
hence A . i in B' by A3, A10, PBOOLE:def 4; :: thesis: verum

end;

hence A . i in (meet SF) . i by A5, A6, SETFAM_1:58; :: thesis: verum