:: deftheorem defines transitive YELLOW_0:def 2 :
for A being RelStr holds
( A is transitive iff for x, y, z being Element of A st x <= y & y <= z holds
x <= z );