let x, X, y be set ; :: thesis: ( x in X \/ {y} iff ( x in X or x = y ) )
( ( not x in X \/ {y} or x in X or x in {y} ) & ( ( x in X or x in {y} ) implies x in X \/ {y} ) & ( x in {y} implies x = y ) & ( x = y implies x in {y} ) ) by TARSKI:def 1, XBOOLE_0:def 3;
hence ( x in X \/ {y} iff ( x in X or x = y ) ) ; :: thesis: verum