theorem ord3: :: REALALG1:25

for R being preordered Ring
for P being Preordering of R holds
( 0. R in P & 1. R in P )