theorem :: REALALG1:32

for R being ordered Ring
for Q being total_OrderRelation of R holds Positives Q is Ordering of R ;