the InternalRel of RS in the entourages of (RelStr2UniformSpaceStr RS) ;
hence the InternalRel of RS is Element of the entourages of (RelStr2UniformSpaceStr RS) ; :: thesis: verum