let R, S be RelStr ; for a, b being object 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 object ; ( ( [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) )
( [a,b] in the InternalRel of S implies [a,b] in the InternalRel of (R [*] S) )
assume
[a,b] in the InternalRel of S
; [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; verum