theorem :: YELLOW_3:17

for X, Y being non empty reflexive RelStr st [:X,Y:] is transitive holds
( X is transitive & Y is transitive )