let R be ordered Ring; :: thesis: for O, P being Ordering of R st O c= P holds
O = P
let O, P be Ordering of R; :: thesis: ( O c= P implies O = P )
assume AS: O c= P ; :: thesis: O = P
now :: thesis: P c= O
assume not P c= O ; :: thesis: contradiction
then consider a being Element of R such that
A: ( a in P & not a in O ) ;
a in the carrier of R ;
then a in O \/ (- O) by defsp;
then a in - O by A, XBOOLE_0:def 3;
then B: - a in - (- O) ;
- a in - P by A;
then - a in P /\ (- P) by AS, B, XBOOLE_0:def 4;
then - a in {(0. R)} by defneg;
then C: - a = 0. R by TARSKI:def 1;
a = - (- a)
.= 0. R by C ;
hence contradiction by A, ord3; :: thesis: verum
end;
hence O = P by AS; :: thesis: verum