:: deftheorem Def1 defines is_serial_in ROUGHS_2:def 1 :
for R being Relation
for X being set holds
( R is_serial_in X iff for x being object st x in X holds
ex y being object st
( y in X & [x,y] in R ) );