let x, y be object ; :: thesis: for X being set st [x,y] in X holds
( x in union (union X) & y in union (union X) )
let X be set ; :: thesis: ( [x,y] in X implies ( x in union (union X) & y in union (union X) ) )
assume A1: [x,y] in X ; :: thesis: ( x in union (union X) & y in union (union X) )
{x} in {{x},{x,y}} by TARSKI:def 2;
then A2: {x} in union X by A1, TARSKI:def 4;
{x,y} in {{x},{x,y}} by TARSKI:def 2;
then A3: {x,y} in union X by A1, TARSKI:def 4;
( y in {x,y} & x in {x} ) by TARSKI:def 1, TARSKI:def 2;
hence ( x in union (union X) & y in union (union X) ) by A3, A2, TARSKI:def 4; :: thesis: verum