let x, y, z be set ; :: thesis: ( x <> y & x <> z implies {x,y,z} \ {x} = {y,z} )
assume A1: ( x <> y & x <> z ) ; :: thesis: {x,y,z} \ {x} = {y,z}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {y,z} c= {x,y,z} \ {x}

let a be set ; :: thesis: ( a in {x,y,z} \ {x} implies a in {y,z} )
assume a in {x,y,z} \ {x} ; :: thesis: a in {y,z}
then ( a in {x,y,z} & not a in {x} ) by XBOOLE_0:def 5;
then ( ( a = x or a = y or a = z ) & a <> x ) by Def1, TARSKI:def 1;
hence a in {y,z} by TARSKI:def 2; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {y,z} or a in {x,y,z} \ {x} )
assume a in {y,z} ; :: thesis: a in {x,y,z} \ {x}
then ( a = y or a = z ) by TARSKI:def 2;
then ( a in {x,y,z} & not a in {x} ) by A1, Def1, TARSKI:def 1;
hence a in {x,y,z} \ {x} by XBOOLE_0:def 5; :: thesis: verum