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