let I be set ; :: thesis: for M being ManySortedSet of I

for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) (/\) (MSUnion B)

let M be ManySortedSet of I; :: 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 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

for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) (/\) (MSUnion B)

let M be ManySortedSet of I; :: 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 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

hence
MSUnion (A /\ B) c= (MSUnion A) (/\) (MSUnion B)
; :: thesis: verum
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 A1, Def2;

for v being object st v in MAB . i holds

v in (MA (/\) MB) . i

end;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 A1, Def2;

for v being object st v in MAB . i holds

v in (MA (/\) MB) . i

proof

hence
MAB . i c= (MA (/\) MB) . i
; :: thesis: verum
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 A3, TARSKI:def 4;

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 A7, XBOOLE_0:def 4;

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 A4, TARSKI:def 4;

g in A by A7, XBOOLE_0:def 4;

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 A4, TARSKI:def 4;

then v in (MA . i) /\ (MB . i) by A2, A8, XBOOLE_0:def 4;

hence v in (MA (/\) MB) . i by A1, PBOOLE:def 5; :: thesis: verum

end;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 A3, TARSKI:def 4;

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 A7, XBOOLE_0:def 4;

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 A4, TARSKI:def 4;

g in A by A7, XBOOLE_0:def 4;

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 A4, TARSKI:def 4;

then v in (MA . i) /\ (MB . i) by A2, A8, XBOOLE_0:def 4;

hence v in (MA (/\) MB) . i by A1, PBOOLE:def 5; :: thesis: verum