let R, S be RelStr ; :: thesis: for a, b being set st the carrier of R /\ the carrier of S is lower Subset of S & [a,b] in the InternalRel of (R [*] S) & b in the carrier of R holds
a in the carrier of R
let a, b be set ; :: thesis: ( the carrier of R /\ the carrier of S is lower Subset of S & [a,b] in the InternalRel of (R [*] S) & b in the carrier of R implies a in the carrier of R )
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 lower Subset of S and
A2: [a,b] in the InternalRel of (R [*] S) and
A3: b in the carrier of R ; :: thesis: a in the carrier of R
[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 a in the carrier of R ; :: thesis: contradiction

per cases ( [a,b] in the InternalRel of S or [a,b] in the InternalRel of R 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 S ; :: thesis: contradiction

then reconsider a9 = a, b9 = b as Element of S by ZFMISC_1:87;
b in the carrier of S by A6, ZFMISC_1:87;
then A7: b in the carrier of R /\ the carrier of S by A3, XBOOLE_0:def 4;
a9 <= b9 by A6, ORDERS_2:def 5;
then a in X by A1, A7, WAYBEL_0:def 19;
hence contradiction by A5; :: thesis: verum

end;

suppose [a,b] in the InternalRel of R ; :: 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;