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

proof

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

end;

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