let V be set ; :: thesis: for M being non empty MetrStruct holds
( V in M -neighbour iff V is equivalence_class of M )
let M be non empty MetrStruct ; :: thesis: ( V in M -neighbour iff V is equivalence_class of M )
A1: ( V is equivalence_class of M implies V in M -neighbour )

proof

assume V is equivalence_class of M ; :: thesis: V in M -neighbour
then ex x being Element of M st V = x -neighbour by Def3;
hence V in M -neighbour ; :: thesis: verum

end;

( V in M -neighbour implies V is equivalence_class of M )

proof

assume V in M -neighbour ; :: thesis: V is equivalence_class of M
then ex x being Element of M st V = x -neighbour by Th15;
hence V is equivalence_class of M by Def3; :: thesis: verum

end;

hence ( V in M -neighbour iff V is equivalence_class of M ) by A1; :: thesis: verum