for Y, SFX being set st SFX is_finer_than {Y} holds
for X being set st X in SFX holds
X c= Y