set Q = OrdRel P;

now :: thesis: for r1, r2, r3 being Element of R st r1 <=_ OrdRel P,r2 holds
r1 + r3 <=_ OrdRel P,r2 + r3

let r1, r2, r3 be Element of R; :: thesis: ( r1 <=_ OrdRel P,r2 implies r1 + r3 <=_ OrdRel P,r2 + r3 )
assume r1 <=_ OrdRel P,r2 ; :: thesis: r1 + r3 <=_ OrdRel P,r2 + r3
then consider a, b being Element of R such that
A: ( [a,b] = [r1,r2] & a <= P,b ) ;
B: ( a = r1 & b = r2 ) by A, XTUPLE_0:1;
(r2 + r3) - (r1 + r3) = (r2 + r3) + ((- r3) + (- r1)) by RLVECT_1:31
.= ((r2 + r3) + (- r3)) + (- r1) by RLVECT_1:def 3
.= (r2 + (r3 + (- r3))) + (- r1) by RLVECT_1:def 3
.= (r2 + (0. R)) + (- r1) by RLVECT_1:5
.= r2 - r1 ;
then r1 + r3 <= P,r2 + r3 by A, B;
hence r1 + r3 <=_ OrdRel P,r2 + r3 ; :: thesis: verum

end;

hence OrdRel P is respecting_addition ; :: thesis: OrdRel P is respecting_multiplication
let r1, r2, r3 be Element of R; :: according to REALALG1:def 4 :: thesis: ( r1 <=_ OrdRel P,r2 & 0. R <=_ OrdRel P,r3 implies r1 * r3 <=_ OrdRel P,r2 * r3 )
assume H: ( r1 <=_ OrdRel P,r2 & 0. R <=_ OrdRel P,r3 ) ; :: thesis: r1 * r3 <=_ OrdRel P,r2 * r3
then consider a, b being Element of R such that
A: ( [a,b] = [r1,r2] & a <= P,b ) ;
consider e, f being Element of R such that
B: ( [e,f] = [(0. R),r3] & e <= P,f ) by H;
D: ( r1 = a & r2 = b & e = 0. R & r3 = f ) by A, B, XTUPLE_0:1;
(r2 * r3) - (r1 * r3) = (r2 - r1) * r3 by VECTSP_1:13;
then E: (r2 * r3) - (r1 * r3) in P * P by D, B, A;
P * P c= P by defppc;
then r1 * r3 <= P,r2 * r3 by E;
hence r1 * r3 <=_ OrdRel P,r2 * r3 ; :: thesis: verum