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 S & b in the carrier of S & R tolerates S & S is transitive holds
[a,b] in the InternalRel of S
let a, b be set ; :: thesis: ( [a,b] in the InternalRel of (R [*] S) & a in the carrier of S & b in the carrier of S & R tolerates S & S is transitive implies [a,b] in the InternalRel of S )
assume that
A1: [a,b] in the InternalRel of (R [*] S) and
A2: a in the carrier of S and
A3: b in the carrier of S and
A4: R tolerates S and
A5: S is transitive ; :: thesis: [a,b] in the InternalRel of S
[a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A1, Def2;
then A6: ( [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;
assume A7: not [a,b] in the InternalRel of S ; :: thesis: contradiction

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

suppose A8: [a,b] in the InternalRel of R ; :: thesis: contradiction

then b in the carrier of R by ZFMISC_1:87;
then A9: b in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def 4;
a in the carrier of R by A8, ZFMISC_1:87;
then a in the carrier of R /\ the carrier of S by A2, XBOOLE_0:def 4;
hence contradiction by A4, A7, A8, A9; :: thesis: verum

end;

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

then a in the carrier of R by ZFMISC_1:87;
then A11: a in the carrier of R /\ the carrier of S by A2, XBOOLE_0:def 4;
A12: the InternalRel of S is_transitive_in the carrier of S by A5, ORDERS_2:def 3;
consider z being object such that
A13: [a,z] in the InternalRel of R and
A14: [z,b] in the InternalRel of S by A10, RELAT_1:def 8;
A15: z in the carrier of S by A14, ZFMISC_1:87;
z in the carrier of R by A13, ZFMISC_1:87;
then z in the carrier of R /\ the carrier of S by A15, XBOOLE_0:def 4;
then [a,z] in the InternalRel of S by A4, A11, A13;
hence contradiction by A2, A3, A7, A14, A15, A12; :: thesis: verum

end;

end;