theorem Th21: :: WAYBEL_0:21

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