theorem :: SETFAM_1:12

for SFX, SFY being set st SFX c= SFY holds
SFX is_finer_than SFY ;