let I be set ; :: thesis: for Z, M being ManySortedSet of I
for SF being non-empty MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
let Z, M be ManySortedSet of I; :: thesis: for SF being non-empty MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
let SF be non-empty MSSubsetFamily of M; :: thesis: ( ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) implies Z c= meet SF )
assume A1: for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ; :: thesis: Z c= meet SF
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or Z . i c= (meet SF) . i )
consider T being ManySortedSet of I such that
A2: T in SF by PBOOLE:134;
assume A3: i in I ; :: thesis: Z . i c= (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 Def1;
A6: for Z9 being set st Z9 in Q holds
Z . i c= Z9

proof

let Z9 be set ; :: thesis: ( Z9 in Q implies Z . i c= Z9 )
assume A7: Z9 in Q ; :: thesis: Z . i c= Z9
dom (T +* (i .--> Z9)) = I by A3, PZFMISC1:1;
then reconsider K = T +* (i .--> Z9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A8: dom (i .--> Z9) = {i} ;
i in {i} by TARSKI:def 1;
then A9: K . i = (i .--> Z9) . i by A8, FUNCT_4:13
.= Z9 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 A10: 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, A7, A9; :: thesis: verum

end;

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

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

end;

end;

end;

then Z c= K by A1;
hence Z . i c= Z9 by A3, A9; :: thesis: verum

end;

Intersect Q = meet Q by A3, A4, SETFAM_1:def 9;
hence Z . i c= (meet SF) . i by A3, A4, A5, A6, SETFAM_1:5; :: thesis: verum