:: deftheorem defines transitive OPOSET_1:def 10 :
for O being non empty RelStr holds
( O is transitive iff the InternalRel of O is transitive Relation of the carrier of O );