let x, y, Z be set ; :: thesis: ( {x,y} misses Z implies not x in Z )
assume that
A1: {x,y} /\ Z = {} and
A2: x in Z ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
then ( x in {x,y} /\ Z or y in {x,y} /\ Z ) by A2, XBOOLE_0:def 4;
hence contradiction by A1; :: thesis: verum