let X be set ; :: thesis: for M being MetrStruct
for a being Point of M
for x being set holds
( x in [:X,(the carrier of M \ {a}):] \/ {[X,a]} iff ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) )
let M be MetrStruct ; :: thesis: for a being Point of M
for x being set holds
( x in [:X,(the carrier of M \ {a}):] \/ {[X,a]} iff ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) )
let a be Point of M; :: thesis: for x being set holds
( x in [:X,(the carrier of M \ {a}):] \/ {[X,a]} iff ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) )
let x be set ; :: thesis: ( x in [:X,(the carrier of M \ {a}):] \/ {[X,a]} iff ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) )
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: ( ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) implies x in [:X,(the carrier of M \ {a}):] \/ {[X,a]} )

proof

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

per cases ( x in [:X,(the carrier of M \ {a}):] or x in {[X,a]} ) by A1, XBOOLE_0:def 3;

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

then consider x1, x2 being set such that
A2: ( x1 in X & x2 in the carrier of M \ {a} & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x2 = x2 as Point of M by A2;
take x1 ; :: thesis: ex b being Point of M st
( x = [x1,b] & ( ( x1 in X & b <> a ) or ( x1 = X & b = a ) ) )
take x2 ; :: thesis: ( x = [x1,x2] & ( ( x1 in X & x2 <> a ) or ( x1 = X & x2 = a ) ) )
thus ( x = [x1,x2] & ( ( x1 in X & x2 <> a ) or ( x1 = X & x2 = a ) ) ) by A2, ZFMISC_1:64; :: thesis: verum

end;

suppose x in {[X,a]} ; :: thesis: ex y being set ex b being Point of M st
( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) )

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: verum

end;

end;

end;

given y being set , b being Point of M such that A3: ( x = [y,b] & ( ( y in X & b <> a ) or ( y = X & b = a ) ) ) ; :: thesis: x in [:X,(the carrier of M \ {a}):] \/ {[X,a]}

per cases ( ( y in X & b <> a ) or ( y = X & b = a ) ) by A3;

suppose A4: ( y in X & b <> a ) ; :: thesis: x in [:X,(the carrier of M \ {a}):] \/ {[X,a]}

not the carrier of M is empty

proof

assume the carrier of M is empty ; :: thesis: contradiction
then ( a = {} & b = {} ) by SUBSET_1:def 2;
hence contradiction by A4; :: thesis: verum

end;

then b in the carrier of M \ {a} by A4, ZFMISC_1:64;
then x in [:X,(the carrier of M \ {a}):] by A3, A4, ZFMISC_1:106;
hence x in [:X,(the carrier of M \ {a}):] \/ {[X,a]} by XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

end;