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