let R, S be RelStr ; :: thesis: for a, b being set st [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive holds
[a,b] in the InternalRel of R
let a, b be set ; :: thesis: ( [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S & R is transitive implies [a,b] in the InternalRel of R )
assume that
A1: ( [a,b] in the InternalRel of (R [*] S) & a in the carrier of R & b in the carrier of R & R tolerates S ) and
A2: R is transitive ; :: thesis: [a,b] in the InternalRel of R
assume A3: not [a,b] in the InternalRel of R ; :: thesis: contradiction
[a,b] in (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by A1, Def2;
then A4: ( [a,b] in the InternalRel of R \/ the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def 3;

per cases ( [a,b] in the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by A3, A4, XBOOLE_0:def 3;

suppose A5: [a,b] in the InternalRel of S ; :: thesis: contradiction

then ( a in the carrier of S & b in the carrier of S ) by ZFMISC_1:106;
then ( a in the carrier of R /\ the carrier of S & b in the carrier of R /\ the carrier of S ) by A1, XBOOLE_0:def 4;
hence contradiction by A1, A3, A5, Def1; :: thesis: verum

end;

suppose A6: [a,b] in the InternalRel of R * the InternalRel of S ; :: thesis: contradiction

then ( a in the carrier of R & b in the carrier of S ) by ZFMISC_1:106;
then A7: b in the carrier of R /\ the carrier of S by A1, XBOOLE_0:def 4;
consider z being set such that
A8: ( [a,z] in the InternalRel of R & [z,b] in the InternalRel of S ) by A6, RELAT_1:def 8;
A9: ( z in the carrier of R & z in the carrier of S ) by A8, ZFMISC_1:106;
then z in the carrier of R /\ the carrier of S by XBOOLE_0:def 4;
then A10: [z,b] in the InternalRel of R by A1, A7, A8, Def1;
the InternalRel of R is_transitive_in the carrier of R by A2, ORDERS_2:def 5;
hence contradiction by A1, A3, A8, A9, A10, RELAT_2:def 8; :: thesis: verum

end;

end;