let M be non empty MetrSpace; :: thesis: for V being Subset of M holds
( V is equivalence_class of M iff ex x being Element of M st V = {x} )
let V be Subset of M; :: thesis: ( V is equivalence_class of M iff ex x being Element of M st V = {x} )
A1: ( V is equivalence_class of M implies ex x being Element of M st V = {x} )

proof

assume V is equivalence_class of M ; :: thesis: ex x being Element of M st V = {x}
then consider x being Element of M such that
A2: V = x -neighbour by Def3;
x -neighbour = {x} by Th13;
hence ex x being Element of M st V = {x} by A2; :: thesis: verum

end;

( ex x being Element of M st V = {x} implies V is equivalence_class of M )

proof

given x being Element of M such that A3: V = {x} ; :: thesis: V is equivalence_class of M
{x} = x -neighbour by Th13;
hence V is equivalence_class of M by A3, Def3; :: thesis: verum

end;

hence ( V is equivalence_class of M iff ex x being Element of M st V = {x} ) by A1; :: thesis: verum