let I be set ; :: thesis: for M being ManySortedSet of
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
let M be ManySortedSet of ; :: thesis: for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
let A, B be SubsetFamily of M; :: thesis: MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
reconsider MAB = MSUnion (A /\ B) as ManySortedSet of ;
reconsider MA = MSUnion A as ManySortedSet of ;
reconsider MB = MSUnion B as ManySortedSet of ;
for i being set st i in I holds
MAB . i c= (MA /\ MB) . i

proof

let i be set ; :: 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: MAB . i = union { (f . i) where f is Element of Bool M : f in A /\ B } by Def4;
A3: MA . i = union { (f . i) where f is Element of Bool M : f in A } by A1, Def4;
A4: MB . i = union { (f . i) where f is Element of Bool M : f in B } by A1, Def4;
for v being set st v in MAB . i holds
v in (MA /\ MB) . i

proof

let v be set ; :: 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
A5: v in w and
A6: w in { (f . i) where f is Element of Bool M : f in A /\ B } by A2, TARSKI:def 4;
consider g being Element of Bool M such that
A7: w = g . i and
A8: g in A /\ B by A6;
( g in A & g in B ) by A8, XBOOLE_0:def 4;
then ( w in { (f . i) where f is Element of Bool M : f in A } & w in { (f . i) where f is Element of Bool M : f in B } ) by A7;
then ( v in union { (f . i) where f is Element of Bool M : f in A } & v in union { (f . i) where f is Element of Bool M : f in B } ) by A5, TARSKI:def 4;
then v in (MA . i) /\ (MB . i) by A3, A4, XBOOLE_0:def 4;
hence v in (MA /\ MB) . i by A1, PBOOLE:def 8; :: thesis: verum

end;

hence MAB . i c= (MA /\ MB) . i by TARSKI:def 3; :: thesis: verum

end;

hence MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) by PBOOLE:def 5; :: thesis: verum