let x, y be object ; :: thesis: for Z being set st {x,y} misses Z holds
not x in Z
let 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