:: deftheorem defines is_coarser_than SETFAM_1:def 3 :
for SFX, SFY being set holds
( SFY is_coarser_than SFX iff for Y being set st Y in SFY holds
ex X being set st
( X in SFX & X c= Y ) );