for X being set
for SF being upper Subset-Family of [:X,X:] st meet SF in SF holds
rho (meet SF) c= SF