let X, Y be set ; :: thesis: union {X,Y} = X \/ Y
for x being object holds
( x in union {X,Y} iff ( x in X or x in Y ) )

proof

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

end;

hence union {X,Y} = X \/ Y by XBOOLE_0:def 3; :: thesis: verum