let C be Convergence-Class of S; :: thesis: C is Relation-like
C is Subset of [:(NetUniv S),the carrier of S:] by Def21;
hence C is Relation-like ; :: thesis: verum