let R be preordered Ring; :: thesis: for P being Preordering of R holds (- P) * P = P * (- P)
let P be Preordering of R; :: thesis: (- P) * P = P * (- P)

A: now :: thesis: for o being object st o in (- P) * P holds
o in P * (- P)

let o be object ; :: thesis: ( o in (- P) * P implies o in P * (- P) )
assume o in (- P) * P ; :: thesis: o in P * (- P)
then consider a, b being Element of R such that
A1: ( o = a * b & a in - P & b in P ) ;
consider c being Element of R such that
A2: ( a = - c & c in P ) by A1;
A3: - b in - P by A1;
c * (- b) = - (c * b) by VECTSP_1:8
.= a * b by A2, VECTSP_1:9 ;
hence o in P * (- P) by A1, A2, A3; :: thesis: verum

end;

now :: thesis: for o being object st o in P * (- P) holds
o in (- P) * P

let o be object ; :: thesis: ( o in P * (- P) implies o in (- P) * P )
assume o in P * (- P) ; :: thesis: o in (- P) * P
then consider a, b being Element of R such that
A1: ( o = a * b & a in P & b in - P ) ;
consider c being Element of R such that
A2: ( b = - c & c in P ) by A1;
A3: - a in - P by A1;
(- a) * c = - (a * c) by VECTSP_1:9
.= a * b by A2, VECTSP_1:8 ;
hence o in (- P) * P by A1, A2, A3; :: thesis: verum

end;

hence (- P) * P = P * (- P) by A, TARSKI:2; :: thesis: verum