let M be non empty MetrSpace; :: thesis: for x being Element of M holds {x} in M -neighbour
let x be Element of M; :: thesis: {x} in M -neighbour
x -neighbour = {x} by Th13;
hence {x} in M -neighbour ; :: thesis: verum