for L being non empty reflexive transitive RelStr
for u, x, y, z being Element of L st u <= x & x << y & y <= z holds
u << z