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 IR = the InternalRel of R, IS = the InternalRel of S as Relation of (the carrier of R \/ the carrier of S) by RELSET_1:17;
A1: the carrier of R c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
A2: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;
then [:the carrier of R,the carrier of S:] c= [:(the carrier of R \/ the carrier of S),(the carrier of R \/ the carrier of S):] by A1, ZFMISC_1:119;
then reconsider IQ = [:the carrier of R,the carrier of S:] as Relation of (the carrier of R \/ the carrier of S) ;
[:the carrier of S,the carrier of R:] c= [:(the carrier of R \/ the carrier of S),(the carrier of R \/ the carrier of S):] by A1, A2, ZFMISC_1:119;
then reconsider IP = [:the carrier of S,the carrier of R:] as Relation of (the carrier of R \/ the carrier of S) ;
set D = ((IR \/ IS) \/ IQ) \/ IP;
take RelStr(# (the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) ; :: thesis: ( the carrier of RelStr(# (the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# (the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = ((the InternalRel of R \/ the InternalRel of S) \/ [:the carrier of R,the carrier of S:]) \/ [:the carrier of S,the carrier of R:] )
thus ( the carrier of RelStr(# (the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = the carrier of R \/ the carrier of S & the InternalRel of RelStr(# (the carrier of R \/ the carrier of S),(((IR \/ IS) \/ IQ) \/ IP) #) = ((the InternalRel of R \/ the InternalRel of S) \/ [:the carrier of R,the carrier of S:]) \/ [:the carrier of S,the carrier of R:] ) ; :: thesis: verum