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