now :: thesis: for x being object holds
( x in {2,3,4} \ {4} iff x in {2,3} )

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

end;

hence {2,3,4} \ {4} = {2,3} by TARSKI:2; :: thesis: verum