let x, y be object ; :: thesis: for X being set st [x,y] in X holds
y in union (union X)
let 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},{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