let X be 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 ) ) ) )
let M be 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 a be 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 x be set ; ( 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 ) ) ) )
( 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]} )
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 ) )
; x in [:X,( the carrier of M \ {a}):] \/ {[X,a]}