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

proof

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

end;

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