thus
{1,2,3} \ {1} c= {2,3}
XBOOLE_0:def 10 {2,3} c= {1,2,3} \ {1}proof
let x be
object ;
TARSKI:def 3 ( not x in {1,2,3} \ {1} or x in {2,3} )
assume
x in {1,2,3} \ {1}
;
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;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {2,3} or x in {1,2,3} \ {1} )
assume
x in {2,3}
; 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; verum