:: deftheorem Def2 defines with_equivalence ROUGHS_1:def 2 :
for P being RelStr holds
( P is with_equivalence iff the InternalRel of P is Equivalence_Relation of the carrier of P );