let x, y be object ; :: thesis: for X being set st [x,y] in X holds
x in union (union X)
let X be set ; :: thesis: ( [x,y] in X implies x in union (union X) )
assume A1: [x,y] in X ; :: thesis: x 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 in {x} by TARSKI:def 1;
hence x in union (union X) by A2, TARSKI:def 4; :: thesis: verum