:: deftheorem Def1 defines EqRel WAYBEL20:def 1 :
for L being RelStr
for R being Subset of [:L,L:] st R is Equivalence_Relation of the carrier of L holds
EqRel R = R;