theorem :: ORDERS_1:42

for R being Relation
for X being set st R linearly_orders X holds
R ~ linearly_orders X by Lm12, Lm13, Lm14, Lm15;