let R be non degenerated preordered Ring; :: thesis: for P being Preordering of R holds not - (1. R) in P
let P be Preordering of R; :: thesis: not - (1. R) in P
A: 1. R in P by ord3;
assume - (1. R) in P ; :: thesis: contradiction
then - (- (1. R)) in - P ;
then 1. R in P /\ (- P) by XBOOLE_0:def 4, A;
then 1. R in {(0. R)} by defppc;
hence contradiction by TARSKI:def 1; :: thesis: verum