let I be set ; :: thesis: for Z, M being ManySortedSet of
for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
let Z, M be ManySortedSet of ; :: thesis: for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF
let SF be V8() MSSubsetFamily of M; :: thesis: ( ( for Z1 being ManySortedSet of st Z1 in SF holds
Z c= Z1 ) implies Z c= meet SF )
assume A1: for Z1 being ManySortedSet of st Z1 in SF holds
Z c= Z1 ; :: thesis: Z c= meet SF
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or Z . i c= (meet SF) . i )
assume A2: i in I ; :: thesis: Z . i c= (meet SF) . 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: Q <> {} by A2, A3;
then A6: Intersect Q = meet Q by SETFAM_1:def 10;
consider T being ManySortedSet of such that
A7: T in SF by PBOOLE:146;
for Z' being set st Z' in Q holds
Z . i c= Z'

proof

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

end;

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

then not q in dom (i .--> Z') 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 Z c= K by A1;
hence Z . i c= Z' by A2, A10, PBOOLE:def 5; :: thesis: verum

end;

hence Z . i c= (meet SF) . i by A4, A5, A6, SETFAM_1:6; :: thesis: verum