for X, Y, SFX being set st SFX is_finer_than {X,Y} holds
for Z being set holds
( not Z in SFX or Z c= X or Z c= Y )