theorem ordsub: :: REALALG1:29

for R being ordered Ring
for O, P being Ordering of R st O c= P holds
O = P