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) & b in the carrier of R ) ; :: thesis: a in the carrier of R
assume A3: not a in the carrier of R ; :: thesis: contradiction
[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;

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 A5: [a,b] in the InternalRel of S ; :: thesis: contradiction

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

end;

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

hence contradiction by A3, ZFMISC_1:106; :: thesis: verum

end;

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

then consider z being set such that
A7: ( [a,z] in the InternalRel of R & [z,b] in the InternalRel of S ) by RELAT_1:def 8;
thus contradiction by A3, A7, ZFMISC_1:106; :: thesis: verum

end;

end;