theorem Th37: :: COMPL_SP:38

for X being set
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 ) ) ) )