let x be object ; :: thesis: ( x in the carrier of R implies [x,x] in OrdRel P )
assume x in the carrier of R ; :: thesis: [x,x] in OrdRel P
then reconsider a = x as Element of R ;
a - a = 0. R by RLVECT_1:15;
then a <= P,a by ord3;
hence [x,x] in OrdRel P ; :: thesis: verum

let x, y be object ; :: thesis: ( x in field (OrdRel P) & y in field (OrdRel P) & [x,y] in OrdRel P & [y,x] in OrdRel P implies x = y )
assume AS: ( x in field (OrdRel P) & y in field (OrdRel P) & [x,y] in OrdRel P & [y,x] in OrdRel P ) ; :: thesis: x = y
then consider a, b being Element of R such that
A1: ( [x,y] = [a,b] & a <= P,b ) ;
consider e, f being Element of R such that
A2: ( [e,f] = [y,x] & e <= P,f ) by AS;
C: ( x = a & y = b & y = e & x = f ) by A1, A2, XTUPLE_0:1;
- (b - a) = a - b by RLVECT_1:33;
then a - b in - P by A1;
then a - b in P /\ (- P) by C, A2, XBOOLE_0:def 4;
then a - b in {(0. R)} by defneg;
then a - b = 0. R by TARSKI:def 1;
hence x = y by C, RLVECT_1:21; :: thesis: verum

let x, y, z be object ; :: thesis: ( x in field (OrdRel P) & y in field (OrdRel P) & z in field (OrdRel P) & [x,y] in OrdRel P & [y,z] in OrdRel P implies [x,z] in OrdRel P )
assume AS: ( x in field (OrdRel P) & y in field (OrdRel P) & z in field (OrdRel P) & [x,y] in OrdRel P & [y,z] in OrdRel P ) ; :: thesis: [x,z] in OrdRel P
then consider a, b being Element of R such that
A1: ( [x,y] = [a,b] & a <= P,b ) ;
consider e, c being Element of R such that
A2: ( [e,c] = [y,z] & e <= P,c ) by AS;
C: ( x = a & y = b & y = e & z = c ) by A1, A2, XTUPLE_0:1;
then (c - b) + (b - a) in { (s1 + s2) where s1, s2 is Element of R : ( s1 in P & s2 in P ) } by A1, A2;
then D: (c - b) + (b - a) in P + P by IDEAL_1:def 19;
B: P + P c= P by defppc;
(c - b) + (b - a) = ((c + (- b)) + b) + (- a) by RLVECT_1:def 3
.= (c + ((- b) + b)) + (- a) by RLVECT_1:def 3
.= (c + (0. R)) + (- a) by RLVECT_1:5
.= c - a ;
then a <= P,c by B, D;
hence [x,z] in OrdRel P by C; :: thesis: verum