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) and
A2: a in the carrier of R and
A3: b in the carrier of R and
A4: R tolerates S and
A5: R is transitive ; :: thesis: [a,b] in the InternalRel of R
[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 R ; :: thesis: contradiction
per cases ( [a,b] in the InternalRel of S 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 S ; :: thesis: contradiction
then b in the carrier of S 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 S 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 b in the carrier of S by ZFMISC_1:87;
then A11: b in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def 4;
A12: the InternalRel of R is_transitive_in the carrier of R 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 R by A13, ZFMISC_1:87;
z in the carrier of S by A14, ZFMISC_1:87;
then z in the carrier of R /\ the carrier of S by A15, XBOOLE_0:def 4;
then [z,b] in the InternalRel of R by A4, A11, A14;
hence contradiction by A2, A3, A7, A13, A15, A12; :: thesis: verum
end;
end;