:: deftheorem defmax defines maximal REALALG2:def 1 :
for R being preordered Ring
for P being Preordering of R holds
( P is maximal iff for Q being Preordering of R st P c= Q holds
P = Q );