let R be preordered Ring; :: thesis: for P being Preordering of R holds
( (- P) + (- P) c= - P & (- P) * (- P) c= P )
let P be Preordering of R; :: thesis: ( (- P) + (- P) c= - P & (- P) * (- P) c= P )
X: ( P + P c= P & P * P c= P ) by REALALG1:def 14;
hereby :: according to TARSKI:def 3 :: thesis: (- P) * (- P) c= P
let o be object ; :: thesis: ( o in (- P) + (- P) implies o in - P )
assume o in (- P) + (- P) ; :: thesis: o in - P
then consider a, b being Element of R such that
A: ( o = a + b & a in - P & b in - P ) ;
( - a in - (- P) & - b in - (- P) ) by A;
then (- a) + (- b) in P + P ;
then (- a) + (- b) in P by X;
then - (a + b) in P by RLVECT_1:31;
then - (- (a + b)) in - P ;
hence o in - P by A; :: thesis: verum
end;
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (- P) * (- P) or o in P )
assume o in (- P) * (- P) ; :: thesis: o in P
then consider a, b being Element of R such that
A: ( o = a * b & a in - P & b in - P ) ;
( - a in - (- P) & - b in - (- P) ) by A;
then (- a) * (- b) in P * P ;
then (- a) * (- b) in P by X;
hence o in P by A, VECTSP_1:10; :: thesis: verum