theorem c1: :: REALALG2:43

for R being preordered Ring
for P being Preordering of R
for a being Element of R holds a <= P,a