let L be RelStr ; :: thesis: ( L is with_equivalence implies L is with_tolerance )
assume L is with_equivalence ; :: thesis: L is with_tolerance
then the InternalRel of L is Equivalence_Relation of by Def2;
hence L is with_tolerance by Def3; :: thesis: verum