let I be set ; :: thesis: for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { () where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A

let M be ManySortedSet of I; :: thesis: for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { () where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A

let AA be set ; :: thesis: ( ( for x being set st x in AA holds
x is SubsetFamily of M ) implies for A, B being SubsetFamily of M st B = { () where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A )

assume A1: for x being set st x in AA holds
x is SubsetFamily of M ; :: thesis: for A, B being SubsetFamily of M st B = { () where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A

let A, B be SubsetFamily of M; :: thesis: ( B = { () where X is SubsetFamily of M : X in AA } & A = union AA implies MSUnion B = MSUnion A )
assume that
A2: B = { () where X is SubsetFamily of M : X in AA } and
A3: A = union AA ; :: thesis:
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or () . i = () . i )
assume A4: i in I ; :: thesis: () . i = () . i
thus (MSUnion B) . i c= () . i :: according to XBOOLE_0:def 10 :: thesis: () . i c= () . i
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in () . i or a in () . i )
thus ( a in () . i implies a in () . i ) :: thesis: verum
proof
assume a in () . i ; :: thesis: a in () . i
then a in union { (f . i) where f is Element of Bool M : f in B } by ;
then consider Y being set such that
A5: a in Y and
A6: Y in { (f . i) where f is Element of Bool M : f in B } by TARSKI:def 4;
consider f being Element of Bool M such that
A7: f . i = Y and
A8: f in B by A6;
consider Q being SubsetFamily of M such that
A9: f = MSUnion Q and
A10: Q in AA by A2, A8;
(MSUnion Q) . i = union { (g . i) where g is Element of Bool M : g in Q } by ;
then consider d being set such that
A11: a in d and
A12: d in { (g . i) where g is Element of Bool M : g in Q } by ;
consider g being Element of Bool M such that
A13: d = g . i and
A14: g in Q by A12;
g in union AA by ;
then d in { (h . i) where h is Element of Bool M : h in union AA } by A13;
then a in union { (h . i) where h is Element of Bool M : h in union AA } by ;
hence a in () . i by A3, A4, Def2; :: thesis: verum
end;
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in () . i or a in () . i )
assume a in () . i ; :: thesis: a in () . i
then a in union { (f . i) where f is Element of Bool M : f in A } by ;
then consider Y being set such that
A15: a in Y and
A16: Y in { (f . i) where f is Element of Bool M : f in A } by TARSKI:def 4;
consider f being Element of Bool M such that
A17: f . i = Y and
A18: f in A by A16;
consider c being set such that
A19: f in c and
A20: c in AA by ;
reconsider c = c as SubsetFamily of M by ;
f . i in { (v . i) where v is Element of Bool M : v in c } by A19;
then A21: a in union { (v . i) where v is Element of Bool M : v in c } by ;
(MSUnion c) . i = union { (v . i) where v is Element of Bool M : v in c } by ;
then consider cos being set such that
A22: a in cos and
A23: cos = () . i by A21;
MSUnion c in { () where X is SubsetFamily of M : X in AA } by A20;
then cos in { (t . i) where t is Element of Bool M : t in B } by ;
then a in union { (t . i) where t is Element of Bool M : t in B } by ;
hence a in () . i by ; :: thesis: verum