:: deftheorem defines serial ROUGHS_2:def 2 :
for R being Relation holds
( R is serial iff R is_serial_in field R );