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

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

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

end;

hence meet SF = V ; :: thesis: verum