let R, S be RelStr ; :: thesis: ( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) )
A1: the InternalRel of R c= the InternalRel of R \/ the InternalRel of S by XBOOLE_1:7;
the InternalRel of R \/ the InternalRel of S c= (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by XBOOLE_1:7;
then the InternalRel of R c= (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by A1, XBOOLE_1:1;
hence the InternalRel of R c= the InternalRel of (R [*] S) by Def2; :: thesis: the InternalRel of S c= the InternalRel of (R [*] S)
A2: the InternalRel of S c= the InternalRel of R \/ the InternalRel of S by XBOOLE_1:7;
the InternalRel of R \/ the InternalRel of S c= (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by XBOOLE_1:7;
then the InternalRel of S c= (the InternalRel of R \/ the InternalRel of S) \/ (the InternalRel of R * the InternalRel of S) by A2, XBOOLE_1:1;
hence the InternalRel of S c= the InternalRel of (R [*] S) by Def2; :: thesis: verum