for X being non empty set
for x, y being object
for R1, R2 being Relation
for n, m being Element of NAT st n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st
( len f = n & x,y are_joint_by f,R1,R2 ) holds
ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )