take union {X,Y} ; :: thesis: for x being set holds
( x in union {X,Y} iff ( x in X or x in Y ) )
let x be set ; :: thesis: ( x in union {X,Y} iff ( x in X or x in Y ) )
thus ( not x in union {X,Y} or x in X or x in Y ) :: thesis: ( ( x in X or x in Y ) implies x in union {X,Y} )

proof

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

end;

assume ( x in X or x in Y ) ; :: thesis: x in union {X,Y}
then consider X0 being set such that
A2: ( X0 = X or X0 = Y ) and
A3: x in X0 ;
X0 in {X,Y} by A2, TARSKI:def 2;
hence x in union {X,Y} by A3, TARSKI:def 4; :: thesis: verum