let x be object ; :: thesis:
let X be set ; :: thesis:
assume that
A1: X <> {x} and
A2: X <> {} ; :: thesis:

per cases ;

suppose A3: not x in X ; :: thesis:

consider y being object such that
A4: y in X by A2, XBOOLE_0:7;
take y ; :: thesis:
thus ( y in X & y <> x ) by A3, A4; :: thesis:

end;

suppose A5: x in X ; :: thesis:

consider y being object such that
A6: ( ( y in X & not y in {x} ) or ( y in {x} & not y in X ) ) by A1, TARSKI:2;
take y ; :: thesis:
thus ( y in X & y <> x ) by A5, A6, TARSKI:def 1; :: thesis:

end;

end;