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