now :: thesis: for x being object holds
( x in {2} \ {1,2,3,4} iff contradiction )

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

end;

hence {2} \ {1,2,3,4} = {} by XBOOLE_0:def 1; :: thesis: verum