let R be preordered domRing; :: thesis: for P being Preordering of R holds
( (P ^-) * (P ^-) c= P ^+ & (P ^+) * (P ^-) c= P ^- & (P ^-) * (P ^+) c= P ^- )
let P be Preordering of R; :: thesis: ( (P ^-) * (P ^-) c= P ^+ & (P ^+) * (P ^-) c= P ^- & (P ^-) * (P ^+) c= P ^- )

now :: thesis: for o being object st o in (P ^-) * (P ^-) holds
o in 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: ( a in - P & not a in {(0. R)} & b in - P & not b in {(0. R)} ) by A, XBOOLE_0:def 5;
then C: ( a <> 0. R & b <> 0. R ) by TARSKI:def 1;
D: ( (- P) * (- P) c= P & o in (- P) * (- P) ) by A, B, REALALG2:17;

now :: thesis: not a * b in {(0. R)}

assume a * b in {(0. R)} ; :: thesis: contradiction
then a * b = 0. R by TARSKI:def 1;
hence contradiction by C, VECTSP_2:def 1; :: thesis: verum

end;

hence o in P ^+ by D, A, XBOOLE_0:def 5; :: thesis: verum

end;

hence (P ^-) * (P ^-) c= P ^+ ; :: thesis: ( (P ^+) * (P ^-) c= P ^- & (P ^-) * (P ^+) c= P ^- )

now :: thesis: for o being object st o in (P ^+) * (P ^-) holds
o in 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: ( a in P & not a in {(0. R)} & b in - P & not b in {(0. R)} ) by A, XBOOLE_0:def 5;
then C: ( a <> 0. R & b <> 0. R ) by TARSKI:def 1;
D: ( P * (- P) c= - P & o in P * (- P) ) by A, B, REALALG2:18;

now :: thesis: not a * b in {(0. R)}

assume a * b in {(0. R)} ; :: thesis: contradiction
then a * b = 0. R by TARSKI:def 1;
hence contradiction by C, VECTSP_2:def 1; :: thesis: verum

end;

hence o in P ^- by D, A, XBOOLE_0:def 5; :: thesis: verum

end;

hence (P ^+) * (P ^-) c= P ^- ; :: thesis: (P ^-) * (P ^+) c= P ^-

now :: thesis: for o being object st o in (P ^-) * (P ^+) holds
o in 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: ( a in - P & not a in {(0. R)} & b in P & not b in {(0. R)} ) by A, XBOOLE_0:def 5;
then C: ( a <> 0. R & b <> 0. R ) by TARSKI:def 1;
D: ( (- P) * P c= - P & o in (- P) * P ) by A, B, REALALG2:18;

now :: thesis: not a * b in {(0. R)}

assume a * b in {(0. R)} ; :: thesis: contradiction
then a * b = 0. R by TARSKI:def 1;
hence contradiction by C, VECTSP_2:def 1; :: thesis: verum

end;

hence o in P ^- by D, A, XBOOLE_0:def 5; :: thesis: verum

end;

hence (P ^-) * (P ^+) c= P ^- ; :: thesis: verum