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

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

end;

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