let x, y be object ; :: thesis: for X being set st not x in X & not y in X holds
{x,y} misses X
let X be set ; :: thesis: ( not x in X & not y in X implies {x,y} misses X )
assume A1: ( not x in X & not y in X ) ; :: thesis: {x,y} misses X
thus {x,y} /\ X c= {} :: according to XBOOLE_0:def 7,XBOOLE_0:def 10 :: thesis: {} c= {x,y} /\ X

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y} /\ X or z in {} )
assume z in {x,y} /\ X ; :: thesis: z in {}
then ( z in {x,y} & z in X ) by XBOOLE_0:def 4;
hence z in {} by A1, TARSKI:def 2; :: thesis: verum

end;

thus {} c= {x,y} /\ X ; :: thesis: verum