let x, y be object ; :: thesis: for X being set holds
( x in union {X,{y}} iff ( x in X or x = y ) )
let X be set ; :: thesis: ( x in union {X,{y}} iff ( x in X or x = y ) )
A1: ( not x in union {X,{y}} or x in X or x in {y} )

proof

assume x in union {X,{y}} ; :: thesis: ( x in X or x in {y} )
then ex Z being set st
( x in Z & Z in {X,{y}} ) by TARSKI:def 4;
hence ( x in X or x in {y} ) by TARSKI:def 2; :: thesis: verum

end;

A2: ( x in {y} iff x = y ) by TARSKI:def 1;
( X in {X,{y}} & {y} in {X,{y}} ) by TARSKI:def 2;
hence ( x in union {X,{y}} iff ( x in X or x = y ) ) by A1, A2, TARSKI:def 4; :: thesis: verum