for X, Y being set holds
( X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y )