for X being set st X in fin_RelStr_sp holds
X is non empty finite strict RelStr