theorem Th29: :: UNIFORM3:57
for X being set
for SF being Subset-Family of [:X,X:]
for R being Relation of X st SF = rho R holds
SF c= rho (meet SF)