let R, S be RelStr ; :: thesis: for a, b being set holds
( ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) & ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) ) )
let a, b be set ; :: thesis: ( ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) & ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) ) )
thus ( [a,b] in the InternalRel of R implies [a,b] in the InternalRel of (R [*] S) ) :: thesis: ( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) )

proof

assume [a,b] in the InternalRel of R ; :: thesis: [a,b] in the InternalRel of (R [*] S)
then [a,b] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;
then [a,b] in (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;
hence [a,b] in the InternalRel of (R [*] S) by Def2; :: thesis: verum

end;

assume [a,b] in the InternalRel of S ; :: thesis: [a,b] in the InternalRel of (R [*] S)
then [a,b] in the InternalRel of R \/ the InternalRel of S by XBOOLE_0:def 3;
then [a,b] in (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;
hence [a,b] in the InternalRel of (R [*] S) by Def2; :: thesis: verum