let A be set ; :: thesis: varcl (union A) = union { (varcl a) where a is Element of A : verum }
set X = { (varcl a) where a is Element of A : verum } ;
A1: union A c= union { (varcl a) where a is Element of A : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in union { (varcl a) where a is Element of A : verum } )
assume x in union A ; :: thesis: x in union { (varcl a) where a is Element of A : verum }
then consider Y being set such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
reconsider Y = Y as Element of A by A3;
A4: Y c= varcl Y by Def1;
varcl Y in { (varcl a) where a is Element of A : verum } ;
hence x in union { (varcl a) where a is Element of A : verum } by A2, A4, TARSKI:def 4; :: thesis: verum

end;

now :: thesis: for x, y being set st [x,y] in union { (varcl a) where a is Element of A : verum } holds
x c= union { (varcl a) where a is Element of A : verum }

let x, y be set ; :: thesis: ( [x,y] in union { (varcl a) where a is Element of A : verum } implies x c= union { (varcl a) where a is Element of A : verum } )
assume [x,y] in union { (varcl a) where a is Element of A : verum } ; :: thesis: x c= union { (varcl a) where a is Element of A : verum }
then consider Y being set such that
A5: [x,y] in Y and
A6: Y in { (varcl a) where a is Element of A : verum } by TARSKI:def 4;
ex a being Element of A st Y = varcl a by A6;
then A7: x c= Y by A5, Def1;
Y c= union { (varcl a) where a is Element of A : verum } by A6, ZFMISC_1:74;
hence x c= union { (varcl a) where a is Element of A : verum } by A7; :: thesis: verum

end;

hence varcl (union A) c= union { (varcl a) where a is Element of A : verum } by A1, Def1; :: according to XBOOLE_0:def 10 :: thesis: union { (varcl a) where a is Element of A : verum } c= varcl (union A)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (varcl a) where a is Element of A : verum } or x in varcl (union A) )
assume x in union { (varcl a) where a is Element of A : verum } ; :: thesis: x in varcl (union A)
then consider Y being set such that
A8: x in Y and
A9: Y in { (varcl a) where a is Element of A : verum } by TARSKI:def 4;
consider a being Element of A such that
A10: Y = varcl a by A9;
( A is empty or not A is empty ) ;
then ( a in A or a is empty ) by SUBSET_1:def 1;
then a c= union A by ZFMISC_1:74;
then Y c= varcl (union A) by A10, Th9;
hence x in varcl (union A) by A8; :: thesis: verum