theorem Th22: :: WAYBEL_0:22

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