let x, y be object ; :: thesis: for Z being set st not x in Z & not y in Z holds
{x,y} misses Z
let Z be set ; :: thesis: ( not x in Z & not y in Z implies {x,y} misses Z )
assume A1: ( not x in Z & not y in Z ) ; :: thesis: {x,y} misses Z
assume {x,y} meets Z ; :: thesis: contradiction
then consider z being object such that
A2: z in {x,y} /\ Z by XBOOLE_0:4;
( z in {x,y} & z in Z ) by A2, XBOOLE_0:def 4;
hence contradiction by A1, TARSKI:def 2; :: thesis: verum