theorem avb6: :: REALALG2:56

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;