let x, y, Z be set ; :: thesis: ( [x,y] in Z implies ( x in union (union Z) & y in union (union Z) ) )
assume A1: [x,y] in Z ; :: thesis: ( x in union (union Z) & y in union (union Z) )
set xy = [x,y];
{x,y} in [x,y] by TARSKI:def 2;
then A2: {x,y} in union Z by A1, TARSKI:def 4;
{x} in [x,y] by TARSKI:def 2;
then A3: {x} in union Z by A1, TARSKI:def 4;
( y in {x,y} & x in {x} ) by TARSKI:def 1, TARSKI:def 2;
hence ( x in union (union Z) & y in union (union Z) ) by A2, A3, TARSKI:def 4; :: thesis: verum