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

now :: thesis: for i being object st i in I holds
(meet SF) . i = M . i

let i be object ; :: thesis: ( i in I implies (meet SF) . i = M . i )
assume i in I ; :: thesis: (meet SF) . i = M . i
then consider Q being Subset-Family of (M . i) such that
A2: Q = SF . i and
A3: (meet SF) . i = Intersect Q by Def1;
Q = {} by A1, A2;
hence (meet SF) . i = M . i by A3, SETFAM_1:def 9; :: thesis: verum

end;

hence meet SF = M ; :: thesis: verum