let I be set ; :: thesis: for A, M being ManySortedSet of I
for SF being non-empty MSSubsetFamily of M st A in M & ( for B being ManySortedSet of I st B in SF holds
A in B ) holds
A in meet SF
let A, M be ManySortedSet of I; :: thesis: for SF being non-empty MSSubsetFamily of M st A in M & ( for B being ManySortedSet of I st B in SF holds
A in B ) holds
A in meet SF
let SF be non-empty MSSubsetFamily of M; :: thesis: ( A in M & ( for B being ManySortedSet of I 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 I st B in SF holds
A in B ; :: thesis: A in meet SF
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in (meet SF) . i )
consider T being ManySortedSet of I such that
A3: T in SF by PBOOLE:134;
assume A4: i in I ; :: thesis: A . i in (meet SF) . i
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

proof

let B9 be set ; :: thesis: ( B9 in Q implies A . i in B9 )
assume A8: B9 in Q ; :: thesis: A . i in B9
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

proof

let q be object ; :: according to PBOOLE:def 1 :: 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 A5, A8, A10; :: thesis: verum

end;

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

then not q in dom (i .--> B9) by TARSKI:def 1;
then K . q = T . q by FUNCT_4:11;
hence K . q in SF . q by A3, A11; :: thesis: verum

end;

end;

end;

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

end;

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