let X be set ; :: thesis: for a being Subset-Family of X holds union (union a) = union { (union A) where A is Subset of X : A in a }

let a be Subset-Family of X; :: thesis: union (union a) = union { (union A) where A is Subset of X : A in a }

thus union (union a) c= union { (union A) where A is Subset of X : A in a } :: according to XBOOLE_0:def 10 :: thesis: union { (union A) where A is Subset of X : A in a } c= union (union a)

assume e in union { (union A) where A is Subset of X : A in a } ; :: thesis: e in union (union a)

then consider c being set such that

A6: e in c and

A7: c in { (union A) where A is Subset of X : A in a } by TARSKI:def 4;

consider A being Subset of X such that

A8: c = union A and

A9: A in a by A7;

consider b being set such that

A10: e in b and

A11: b in A by A6, A8, TARSKI:def 4;

b in union a by A9, A11, TARSKI:def 4;

hence e in union (union a) by A10, TARSKI:def 4; :: thesis: verum

let a be Subset-Family of X; :: thesis: union (union a) = union { (union A) where A is Subset of X : A in a }

thus union (union a) c= union { (union A) where A is Subset of X : A in a } :: according to XBOOLE_0:def 10 :: thesis: union { (union A) where A is Subset of X : A in a } c= union (union a)

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union { (union A) where A is Subset of X : A in a } or e in union (union a) )
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in union (union a) or e in union { (union A) where A is Subset of X : A in a } )

assume e in union (union a) ; :: thesis: e in union { (union A) where A is Subset of X : A in a }

then consider B being set such that

A1: e in B and

A2: B in union a by TARSKI:def 4;

consider C being set such that

A3: B in C and

A4: C in a by A2, TARSKI:def 4;

A5: union C in { (union A) where A is Subset of X : A in a } by A4;

e in union C by A1, A3, TARSKI:def 4;

hence e in union { (union A) where A is Subset of X : A in a } by A5, TARSKI:def 4; :: thesis: verum

end;assume e in union (union a) ; :: thesis: e in union { (union A) where A is Subset of X : A in a }

then consider B being set such that

A1: e in B and

A2: B in union a by TARSKI:def 4;

consider C being set such that

A3: B in C and

A4: C in a by A2, TARSKI:def 4;

A5: union C in { (union A) where A is Subset of X : A in a } by A4;

e in union C by A1, A3, TARSKI:def 4;

hence e in union { (union A) where A is Subset of X : A in a } by A5, TARSKI:def 4; :: thesis: verum

assume e in union { (union A) where A is Subset of X : A in a } ; :: thesis: e in union (union a)

then consider c being set such that

A6: e in c and

A7: c in { (union A) where A is Subset of X : A in a } by TARSKI:def 4;

consider A being Subset of X such that

A8: c = union A and

A9: A in a by A7;

consider b being set such that

A10: e in b and

A11: b in A by A6, A8, TARSKI:def 4;

b in union a by A9, A11, TARSKI:def 4;

hence e in union (union a) by A10, TARSKI:def 4; :: thesis: verum