for X being set
for SF being upper Subset-Family of [:X,X:]
for R being Relation of X st R in SF & SF = rho R & meet SF in SF holds
rho (meet SF) = SF by Th29, Th30;