set Q = OrdRel P;
now for r1, r2, r3 being Element of R st r1 <=_ OrdRel P,r2 holds
r1 + r3 <=_ OrdRel P,r2 + r3let r1,
r2,
r3 be
Element of
R;
( r1 <=_ OrdRel P,r2 implies r1 + r3 <=_ OrdRel P,r2 + r3 )assume
r1 <=_ OrdRel P,
r2
;
r1 + r3 <=_ OrdRel P,r2 + r3then 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
;
verum end;
hence
OrdRel P is respecting_addition
; OrdRel P is respecting_multiplication
let r1, r2, r3 be Element of R; REALALG1:def 4 ( 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 )
; 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
; verum