for F being preordered Field
for P being Preordering of F ex O being Ordering of F st P c= O