for R being non empty finite RelStr st R is satisfying(7L') holds
R is satisfying(7H')