for R being non empty reflexive transitive RelStr
for x, y being Element of R holds
( x << y iff downarrow x c= waybelow y )