take union {X,Y} ; :: thesis: for x being object holds
( x in union {X,Y} iff ( x in X or x in Y ) )
let x be object ; :: 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 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;
( X in {X,Y} & Y in {X,Y} ) by TARSKI:def 2;
hence ( ( x in X or x in Y ) implies x in union {X,Y} ) by TARSKI:def 4; :: thesis: verum