for A, B being set
for FR being Subset-Family of [:A,B:]
for A, B being set
for X being Subset of A holds { (R .:^ X) where R is Subset of [:A,B:] : R in FR } is Subset-Family of B