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

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

let i be object ; :: thesis: ( i in I implies (meet SF) . i = (V (/\) W) . i )
assume A2: i in I ; :: thesis: (meet SF) . i = (V (/\) W) . i
then ex Q being Subset-Family of (M . i) st
( Q = SF . i & (meet SF) . i = Intersect Q ) by Def1;
hence (meet SF) . i = meet ({V,W} . i) by A1, A2, SETFAM_1:def 9
.= meet {(V . i),(W . i)} by A2, PZFMISC1:def 2
.= (V . i) /\ (W . i) by SETFAM_1:11
.= (V (/\) W) . i by A2, PBOOLE:def 5 ;
:: thesis: verum

end;

hence meet SF = V (/\) W ; :: thesis: verum