A3: R is_transitive_in field R by Def16;
A4: P is_transitive_in field P by Def16;
let a be set ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being set 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 set ; :: 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
A5: [a,b] in P /\ R and
A6: [b,c] in P /\ R ; :: thesis: [a,c] in P /\ R
A7: [b,c] in R by A6, XBOOLE_0:def 4;
then A8: c in field R by RELAT_1:15;
A9: [a,b] in R by A5, XBOOLE_0:def 4;
then ( a in field R & b in field R ) by RELAT_1:15;
then A10: [a,c] in R by A3, A9, A7, A8, Def8;
A11: [b,c] in P by A6, XBOOLE_0:def 4;
then A12: c in field P by RELAT_1:15;
A13: [a,b] in P by A5, XBOOLE_0:def 4;
then ( a in field P & b in field P ) by RELAT_1:15;
then [a,c] in P by A4, A13, A11, A12, Def8;
hence [a,c] in P /\ R by A10, XBOOLE_0:def 4; :: thesis: verum