for A, B being set st A is_finer_than B holds
A \/ B is_finer_than B