let M be PseudoMetricSpace; :: thesis: for V being equivalence_class of M holds V is non empty set
let V be equivalence_class of M; :: thesis: V is non empty set
ex x being Element of M st V = x -neighbour by Def3;
hence V is non empty set by Th4; :: thesis: verum