let R, S be RelStr ; :: thesis: for a, b being set st the carrier of R /\ the carrier of S is upper Subset of R & [a,b] in the InternalRel of (R [*] S) & a in the carrier of S holds
b in the carrier of S
let a, b be set ; :: thesis: ( the carrier of R /\ the carrier of S is upper Subset of R & [a,b] in the InternalRel of (R [*] S) & a in the carrier of S implies b in the carrier of S )
set X = the carrier of R /\ the carrier of S;
reconsider X = the carrier of R /\ the carrier of S as Subset of R by XBOOLE_1:17;
assume that
A1: the carrier of R /\ the carrier of S is upper Subset of R and
A2: [a,b] in the InternalRel of (R [*] S) and
A3: a in the carrier of S ; :: thesis: b in the carrier of S
[a,b] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A2, 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;
assume A5: not b in the carrier of S ; :: thesis: contradiction
per cases ( [a,b] in the InternalRel of R or [a,b] in the InternalRel of S or [a,b] in the InternalRel of R * the InternalRel of S ) by A4, XBOOLE_0:def 3;
suppose A6: [a,b] in the InternalRel of R ; :: thesis: contradiction
then reconsider a9 = a, b9 = b as Element of R by ZFMISC_1:87;
a in the carrier of R by A6, ZFMISC_1:87;
then A7: a in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def 4;
a9 <= b9 by A6, ORDERS_2:def 5;
then ( X c= the carrier of S & b in X ) by A1, A7, WAYBEL_0:def 20, XBOOLE_1:17;
hence contradiction by A5; :: thesis: verum
end;
suppose [a,b] in the InternalRel of S ; :: thesis: contradiction
hence contradiction by A5, ZFMISC_1:87; :: thesis: verum
end;
suppose [a,b] in the InternalRel of R * the InternalRel of S ; :: thesis: contradiction
hence contradiction by A5, ZFMISC_1:87; :: thesis: verum
end;
end;