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