let X be set ; :: thesis:
let M be MetrStruct ; :: thesis:
let a be Point of M; :: thesis:
let x be set ; :: thesis:
thus ( x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} implies ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) ) :: thesis:

proof

assume A1: x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} ; :: thesis:

per cases by A1, XBOOLE_0:def 3;

suppose x in [:X,( the carrier of M \ {a}):] ; :: thesis:

then consider x1, x2 being object such that
A2: x1 in X and
A3: x2 in the carrier of M \ {a} and
A4: x = [x1,x2] by ZFMISC_1:def 2;
reconsider x2 = x2 as Point of M by A3;
reconsider x1 = x1 as set by TARSKI:1;
take x1 ; :: thesis:
take x2 ; :: thesis:
thus ( x = [x1,x2] & ( ( x1 in X & x2 <> a ) or ( x1 = X & x2 = a ) ) ) by A2, A3, A4, ZFMISC_1:56; :: thesis:

end;

suppose x in {[X,a]} ; :: thesis:

then x = [X,a] by TARSKI:def 1;
hence ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) ; :: thesis:

end;

end;

end;

given y being set , b being Point of M such that A5: x = [y,b] and
A6: ( ( y in X & b <> a ) or ( y = X & b = a ) ) ; :: thesis:

per cases by A6;

suppose A7: ( y in X & b <> a ) ; :: thesis:

not the carrier of M is empty

proof

assume A8: the carrier of M is empty ; :: thesis:
then a = {} by SUBSET_1:def 1;
hence contradiction by A7, A8, SUBSET_1:def 1; :: thesis:

end;

then b in the carrier of M \ {a} by A7, ZFMISC_1:56;
then x in [:X,( the carrier of M \ {a}):] by A5, A7, ZFMISC_1:87;
hence x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} by XBOOLE_0:def 3; :: thesis:

end;

suppose ( y = X & b = a ) ; :: thesis:

then x in {[X,a]} by A5, TARSKI:def 1;
hence x in [:X,( the carrier of M \ {a}):] \/ {[X,a]} by XBOOLE_0:def 3; :: thesis:

end;

end;