let R, S be RelStr ; :: thesis: 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 ; :: 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