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