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

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

end;

suppose [a,b] in the InternalRel of S ; :: 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
A8: ( [a,z] in the InternalRel of R & [z,b] in the InternalRel of S ) by RELAT_1:def 8;
thus contradiction by A3, A8, ZFMISC_1:106; :: thesis: verum

end;

end;