for X, Y being set holds INTERSECTION (X,Y) is_finer_than X