for L being non empty transitive RelStr
for x, y being Element of L st x <= y holds
downarrow x c= downarrow y