A1:
R is_transitive_in field R
by Def16;

A2: P is_transitive_in field P by Def16;

let a be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being object st a in field (P /\ R) & y in field (P /\ R) & z in field (P /\ R) & [a,y] in P /\ R & [y,z] in P /\ R holds

[a,z] in P /\ R

let b, c be object ; :: thesis: ( a in field (P /\ R) & b in field (P /\ R) & c in field (P /\ R) & [a,b] in P /\ R & [b,c] in P /\ R implies [a,c] in P /\ R )

assume that

( a in field (P /\ R) & b in field (P /\ R) & c in field (P /\ R) ) and

A3: [a,b] in P /\ R and

A4: [b,c] in P /\ R ; :: thesis: [a,c] in P /\ R

A5: [b,c] in R by A4, XBOOLE_0:def 4;

then A6: c in field R by RELAT_1:15;

A7: [a,b] in R by A3, XBOOLE_0:def 4;

then ( a in field R & b in field R ) by RELAT_1:15;

then A8: [a,c] in R by A1, A7, A5, A6;

A9: [b,c] in P by A4, XBOOLE_0:def 4;

then A10: c in field P by RELAT_1:15;

A11: [a,b] in P by A3, XBOOLE_0:def 4;

then ( a in field P & b in field P ) by RELAT_1:15;

then [a,c] in P by A2, A11, A9, A10;

hence [a,c] in P /\ R by A8, XBOOLE_0:def 4; :: thesis: verum

A2: P is_transitive_in field P by Def16;

let a be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being object st a in field (P /\ R) & y in field (P /\ R) & z in field (P /\ R) & [a,y] in P /\ R & [y,z] in P /\ R holds

[a,z] in P /\ R

let b, c be object ; :: thesis: ( a in field (P /\ R) & b in field (P /\ R) & c in field (P /\ R) & [a,b] in P /\ R & [b,c] in P /\ R implies [a,c] in P /\ R )

assume that

( a in field (P /\ R) & b in field (P /\ R) & c in field (P /\ R) ) and

A3: [a,b] in P /\ R and

A4: [b,c] in P /\ R ; :: thesis: [a,c] in P /\ R

A5: [b,c] in R by A4, XBOOLE_0:def 4;

then A6: c in field R by RELAT_1:15;

A7: [a,b] in R by A3, XBOOLE_0:def 4;

then ( a in field R & b in field R ) by RELAT_1:15;

then A8: [a,c] in R by A1, A7, A5, A6;

A9: [b,c] in P by A4, XBOOLE_0:def 4;

then A10: c in field P by RELAT_1:15;

A11: [a,b] in P by A3, XBOOLE_0:def 4;

then ( a in field P & b in field P ) by RELAT_1:15;

then [a,c] in P by A2, A11, A9, A10;

hence [a,c] in P /\ R by A8, XBOOLE_0:def 4; :: thesis: verum