:: deftheorem defines WellSpace COMPL_SP:def 11 :
for M being MetrStruct
for a being Point of M
for X being set holds WellSpace (a,X) = MetrStruct(# ([:X,( the carrier of M \ {a}):] \/ {[X,a]}),(well_dist (a,X)) #);