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