theorem avb5: :: REALALG2:55

for R being preordered Ring
for P being Preordering of R
for a, b, c being Element of R st a < P,b & b <= P,c holds
a < P,c by c2, c3;