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 } ;
A0: union A c= union { (varcl a) where a is Element of A : verum }

proof

let x be set ; :: 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
A3: ( x in Y & Y in A ) by TARSKI:def 4;
reconsider Y = Y as Element of A by A3;
Y c= varcl Y by VARCL;
then ( varcl Y in { (varcl a) where a is Element of A : verum } & x in varcl Y ) by A3;
hence x in union { (varcl a) where a is Element of A : verum } by TARSKI:def 4; :: thesis: verum

end;

now

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
A1: ( [x,y] in Y & Y in { (varcl a) where a is Element of A : verum } ) by TARSKI:def 4;
consider a being Element of A such that
A2: Y = varcl a by A1;
( x c= Y & Y c= union { (varcl a) where a is Element of A : verum } ) by A1, A2, VARCL, ZFMISC_1:92;
hence x c= union { (varcl a) where a is Element of A : verum } by XBOOLE_1:1; :: thesis: verum

end;

hence varcl (union A) c= union { (varcl a) where a is Element of A : verum } by A0, VARCL; :: according to XBOOLE_0:def 10 :: thesis: union { (varcl a) where a is Element of A : verum } c= varcl (union A)
let x be set ; :: 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
A4: ( x in Y & Y in { (varcl a) where a is Element of A : verum } ) by TARSKI:def 4;
consider a being Element of A such that
A5: Y = varcl a by A4;
( A is empty or not A is empty ) ;
then ( a in A or a is empty ) by SUBSET_1:def 2;
then a c= union A by XBOOLE_1:2, ZFMISC_1:92;
then Y c= varcl (union A) by A5, Th13;
hence x in varcl (union A) by A4; :: thesis: verum