:: deftheorem Def16 defines transitive RELAT_2:def 16 :
for R being Relation holds
( R is transitive iff R is_transitive_in field R );