let P, R be Relation; :: thesis: ( P is transitive & R is transitive implies P /\ R is transitive )
assume that
A1: P is transitive and
A2: R is transitive ; :: thesis: P /\ R is transitive
A3: P is_transitive_in field P by A1, Def16;
A4: R is_transitive_in field R by A2, Def16;

now

let a, 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 & [b,c] in P /\ R ) ; :: thesis: [a,c] in P /\ R
A6: ( [a,b] in P & [a,b] in R & [b,c] in P & [b,c] in R ) by A5, XBOOLE_0:def 4;
then ( a in field P & b in field P & c in field P & a in field R & b in field R & c in field R ) by RELAT_1:30;
then ( [a,c] in P & [a,c] in R ) by A3, A4, A6, Def8;
hence [a,c] in P /\ R by XBOOLE_0:def 4; :: thesis: verum

end;

then P /\ R is_transitive_in field (P /\ R) by Def8;
hence P /\ R is transitive by Def16; :: thesis: verum