Subset_compl:

Add and prove not_in_empty{set,}, in_full{set,}.

Finite_dim:
Add and prove lmS_{injS,bijS}_sub_dim_equiv, lmS_bijS_sub_full_equiv.

FE, FE_simplex:
Remove obsolete sigma_injS_equiv, bijS_equiv_sub_ms
  (use new lmS_bijS_sub_full_equiv instead).