let x, y be object ; :: thesis: for X being set holds
( {x,y} \ X = {} iff ( x in X & y in X ) )
let X be set ; :: thesis: ( {x,y} \ X = {} iff ( x in X & y in X ) )
( {x,y} \ X = {} iff {x,y} c= X ) by XBOOLE_1:37;
hence ( {x,y} \ X = {} iff ( x in X & y in X ) ) by Th31; :: thesis: verum