for R being RelStr st R in fin_RelStr_sp holds
the carrier of R in FinSETS