theorem :: REALALG1:34

for R being ordered Ring
for O being Ordering of R
for S being Subring of R holds O /\ the carrier of S is Ordering of S