A: P * P c= P by REALALG1:def 14;
( a in P \ {(0. R)} & b in P \ {(0. R)} ) by REALALG2:def 8;
then ( a in P & b in P ) by XBOOLE_0:def 5;
then B: a * b in P * P ;

now :: thesis: not a * b = 0. R

assume a * b = 0. R ; :: thesis: contradiction

per cases then ( a = 0. R or b = 0. R ) by VECTSP_2:def 1;

suppose a = 0. R ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose b = 0. R ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

end;

end;

then not a * b in {(0. R)} by TARSKI:def 1;
then a * b in P \ {(0. R)} by A, B, XBOOLE_0:def 5;
hence a * b is P -positive by REALALG2:def 8; :: thesis: verum