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