let x, y, z be set ; :: thesis: ( x <> z & y <> z implies {x,y} \ {z} = {x,y} )
assume that
A1: x <> z and
A2: y <> z ; :: thesis: {x,y} \ {z} = {x,y}
for a being object st a in {x,y} holds
not a in {z}

proof

let a be object ; :: thesis: ( a in {x,y} implies not a in {z} )
assume a in {x,y} ; :: thesis: not a in {z}
then a <> z by A1, A2, TARSKI:def 2;
hence not a in {z} by TARSKI:def 1; :: thesis: verum

end;

then {x,y} misses {z} by XBOOLE_0:3;
hence {x,y} \ {z} = {x,y} by XBOOLE_1:83; :: thesis: verum