for R being Relation
for X, Y being set st R linearly_orders Y & X c= Y holds
R linearly_orders X