let a, b, c be set ; :: thesis: not c in a \ ({c} \/ b)
assume c in a \ ({c} \/ b) ; :: thesis: contradiction
then not c in {c} \/ b by XBOOLE_0:def 5;
then not c in {c} by XBOOLE_0:def 3;
hence contradiction by TARSKI:def 1; :: thesis: verum