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