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

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

end;

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