theorem c2: :: REALALG2:44

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