theorem :: SETFAM_1:20

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