theorem :: YELLOW15:17

for X being set
for Y, Z being finite Subset-Family of X st Z c= Y holds
Components Y is_finer_than Components Z