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)

proof

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;

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) )
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