let I be set ; :: thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= () (/\) ()

let M be ManySortedSet of I; :: thesis: for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= () (/\) ()
let A, B be SubsetFamily of M; :: thesis: MSUnion (A /\ B) c= () (/\) ()
reconsider MAB = MSUnion (A /\ B) as ManySortedSet of I ;
reconsider MA = MSUnion A as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSet of I ;
for i being object st i in I holds
MAB . i c= (MA (/\) MB) . i
proof
let i be object ; :: thesis: ( i in I implies MAB . i c= (MA (/\) MB) . i )
assume A1: i in I ; :: thesis: MAB . i c= (MA (/\) MB) . i
then A2: ( MA . i = union { (f . i) where f is Element of Bool M : f in A } & MB . i = union { (f . i) where f is Element of Bool M : f in B } ) by Def2;
A3: MAB . i = union { (f . i) where f is Element of Bool M : f in A /\ B } by ;
for v being object st v in MAB . i holds
v in (MA (/\) MB) . i
proof
let v be object ; :: thesis: ( v in MAB . i implies v in (MA (/\) MB) . i )
assume v in MAB . i ; :: thesis: v in (MA (/\) MB) . i
then consider w being set such that
A4: v in w and
A5: w in { (f . i) where f is Element of Bool M : f in A /\ B } by ;
consider g being Element of Bool M such that
A6: w = g . i and
A7: g in A /\ B by A5;
g in B by ;
then w in { (f . i) where f is Element of Bool M : f in B } by A6;
then A8: v in union { (f . i) where f is Element of Bool M : f in B } by ;
g in A by ;
then w in { (f . i) where f is Element of Bool M : f in A } by A6;
then v in union { (f . i) where f is Element of Bool M : f in A } by ;
then v in (MA . i) /\ (MB . i) by ;
hence v in (MA (/\) MB) . i by ; :: thesis: verum
end;
hence MAB . i c= (MA (/\) MB) . i ; :: thesis: verum
end;
hence MSUnion (A /\ B) c= () (/\) () ; :: thesis: verum