theorem :: REALALG2:54

for R being ordered Ring
for O being Ordering of R
for a, b being Element of R holds
( a < O,b or b < O,a or a = b ) by avb4;