thus {1,2,3} \ {2,3,4} c= {1} :: according to XBOOLE_0:def 10 :: thesis: {1} c= {1,2,3} \ {2,3,4}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1,2,3} \ {2,3,4} or x in {1} )
assume x in {1,2,3} \ {2,3,4} ; :: thesis: x in {1}
then ( x in {1,2,3} & not x in {2,3,4} ) by XBOOLE_0:def 5;
then ( ( x = 1 or x = 2 or x = 3 ) & not x = 2 & not x = 3 & not x = 4 ) by ENUMSET1:def 1;
hence x in {1} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {1} or x in {1,2,3} \ {2,3,4} )
assume x in {1} ; :: thesis: x in {1,2,3} \ {2,3,4}
then x = 1 by TARSKI:def 1;
then ( x in {1,2,3} & not x in {2,3,4} ) by ENUMSET1:def 1;
hence x in {1,2,3} \ {2,3,4} by XBOOLE_0:def 5; :: thesis: verum