:: deftheorem defines rho UNIFORM3:def 20 :
for X being set
for R being Relation of X holds rho R = { S where S is Subset of [:X,X:] : R c= S } ;