theorem :: ORDERS_1:40

for R being Relation
for X being set st R quasi_orders X holds
R ~ quasi_orders X by Lm12, Lm13;