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