theorem :: ROUGHS_3:28

for R being non empty finite RelStr st R is satisfying(7L') holds
R is serial by Sat7Serial, Sat7Sat;