:: deftheorem defines CLCongruence WAYBEL20:def 2 :
for L being non empty RelStr
for R being Subset of [:L,L:] holds
( R is CLCongruence iff ( R is Equivalence_Relation of the carrier of L & subrelstr R is CLSubFrame of [:L,L:] ) );