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

proof

let a be set ; :: 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, 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