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 the carrier of L by Def2;
hence L is with_tolerance by Def3; :: thesis: verum