theorem Sat7Sat: :: ROUGHS_3:26

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