naming glitch at `closure_subset`

[t6s]

There are

Lemma interior_subset {T} [A : set T] : A° `<=` A
Lemma subset_closure {T} [A : set T] : A `<=` closure A
Lemma closure_subset [T] [A B : set T] : A `<=` B -> closure A `<=` closure B

It looks like the first two are named according to the position of each operator wrt the subset relation.
The third one looks ad-hoc, and especially problematic if we want to add its interior counterpart.

Lemma subset_interior [T] [A B : set T] : A `<=` B -> interior A `<=` interior B

This name would be bad.

[affeldt-aist]

What about closureS instead of closure_subset?
A bit like the following lemma from finset.v:

Lemma setUS A B C : A \subset B -> C :|: A \subset C :|: B.

fyi: @CohenCyril