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) )
( the InternalRel of R c= the InternalRel of R \/ the InternalRel of S & 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 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)
( the InternalRel of S c= the InternalRel of R \/ the InternalRel of S & 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 XBOOLE_1:1;
hence the InternalRel of S c= the InternalRel of (R [*] S) by Def2; :: thesis: verum