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