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 object ; :: thesis: ( a in {x,y,z} \ {x} implies a in {y,z} )
assume A2: a in {x,y,z} \ {x} ; :: thesis: a in {y,z}
then a in {x,y,z} by XBOOLE_0:def 5;
then A3: ( a = x or a = y or a = z ) by Def1;
not a in {x} by A2, XBOOLE_0:def 5;
hence a in {y,z} by A3, TARSKI:def 1, TARSKI:def 2; :: thesis: verum

end;

let a be object ; :: 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 A4: ( a = y or a = z ) by TARSKI:def 2;
then A5: not a in {x} by A1, TARSKI:def 1;
a in {x,y,z} by A4, Def1;
hence a in {x,y,z} \ {x} by A5, XBOOLE_0:def 5; :: thesis: verum