let R be non degenerated Ring; :: thesis: ( R is preordered implies not R is quadratic_complete )
assume R is preordered ; :: thesis: not R is quadratic_complete
then A: not - (1. R) in QS R by REALALG2:def 3;

now :: thesis: not R is quadratic_complete

assume R is quadratic_complete ; :: thesis: contradiction
then B: the carrier of R c= SQ R ;
SQ R c= QS R by REALALG1:18;
hence contradiction by A, B; :: thesis: verum

end;

hence not R is quadratic_complete ; :: thesis: verum