set X = the carrier of R \/ the carrier of S;
( the carrier of R c= the carrier of R \/ the carrier of S & the carrier of S c= the carrier of R \/ the carrier of S ) by XBOOLE_1:7;
then reconsider G = the InternalRel of R * the InternalRel of S as Relation of ( the carrier of R \/ the carrier of S) by RELSET_1:7;
( the carrier of R c= the carrier of R \/ the carrier of S & the carrier of S c= the carrier of R \/ the carrier of S ) by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S as Relation of ( the carrier of R \/ the carrier of S) by RELSET_1:7;
set F = (IR \/ IS) \/ G;
reconsider F = (IR \/ IS) \/ G as Relation of ( the carrier of R \/ the carrier of S) ;
take RelStr(# ( the carrier of R \/ the carrier of S),F #) ; :: thesis: ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),F #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),F #) = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) )
thus ( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),F #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),F #) = ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) ) ; :: thesis: verum