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