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

proof

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

end;

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