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

proof

let x be object ; :: thesis: ( x in {1,2,3,4} \ {1,2} iff x in {3,4} )
thus ( x in {1,2,3,4} \ {1,2} implies x in {3,4} ) :: thesis: ( x in {3,4} implies x in {1,2,3,4} \ {1,2} )

proof

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

end;

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

end;

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