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

proof

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

end;

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