theorem Th11: :: YELLOW_0:11

for L being transitive RelStr
for X being set
for x, y being Element of L st X is_<=_than x & x <= y holds
X is_<=_than y