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