for F being preordered Field
for P being Preordering of F ex Q being Preordering of F st
( P c= Q & Q is maximal )