let I be set ; :: thesis: for M being ManySortedSet of I
for SF being MSSubsetFamily of M st [[0]] I in SF holds
meet SF = [[0]] I
let M be ManySortedSet of I; :: thesis: for SF being MSSubsetFamily of M st [[0]] I in SF holds
meet SF = [[0]] I
let SF be MSSubsetFamily of M; :: thesis: ( [[0]] I in SF implies meet SF = [[0]] I )
assume A1: [[0]] I in SF ; :: thesis: meet SF = [[0]] I

now

let i be set ; :: thesis: ( i in I implies (meet SF) . i = ([[0]] I) . i )
assume A2: i in I ; :: thesis: (meet SF) . i = ([[0]] I) . 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;
([[0]] I) . i in Q by A1, A2, A3, PBOOLE:def 1;
then A5: {} in Q by PBOOLE:5;
([[0]] I) . i in SF . i by A1, A2, PBOOLE:def 1;
then Intersect Q = meet Q by A3, SETFAM_1:def 9;
then Intersect Q = {} by A5, SETFAM_1:4;
hence (meet SF) . i = ([[0]] I) . i by A4, PBOOLE:5; :: thesis: verum

end;

hence meet SF = [[0]] I by PBOOLE:3; :: thesis: verum