theorem :: SETFAM_1:22

for SFX being set holds DIFFERENCE (SFX,SFX) is_finer_than SFX