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 )

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 ) ;
- b in - P by A;
then B: a * (- b) in (- P) * (- P) by A;
(- P) * (- P) c= P by v1;
then a * (- b) in P by B;
then - (a * b) in P by VECTSP_1:8;
then - (- (a * b)) in - P ;
hence o in - P by A; :: thesis: verum

end;

then (- P) * P c= - P ;
hence P * (- P) c= - P by v1a; :: thesis: verum