:: deftheorem defines serial ROUGHS_2:def 4 :
for R being non empty RelStr holds
( R is serial iff for x being Element of R ex y being Element of R st x <= y );