:: deftheorem Def3 defines serial ROUGHS_2:def 3 :
for R being RelStr holds
( R is serial iff the InternalRel of R is_serial_in the carrier of R );