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