theorem :: RELAT_2:27

for R being Relation holds
( R is transitive iff R * R c= R )