set X = the carrier of R \/ the carrier of S;

A1: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;

A2: the carrier of R c= the carrier of R \/ the carrier of S by XBOOLE_1:7;

then reconsider IQ = [: the carrier of R, the carrier of S:] as Relation of ( the carrier of R \/ the carrier of S) by A1, ZFMISC_1:96;

reconsider IP = [: the carrier of S, the carrier of R:] as Relation of ( the carrier of R \/ the carrier of S) by A2, A1, ZFMISC_1:96;

A3: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;

the carrier of R 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 A3, RELSET_1:7;

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

A1: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;

A2: the carrier of R c= the carrier of R \/ the carrier of S by XBOOLE_1:7;

then reconsider IQ = [: the carrier of R, the carrier of S:] as Relation of ( the carrier of R \/ the carrier of S) by A1, ZFMISC_1:96;

reconsider IP = [: the carrier of S, the carrier of R:] as Relation of ( the carrier of R \/ the carrier of S) by A2, A1, ZFMISC_1:96;

A3: the carrier of S c= the carrier of R \/ the carrier of S by XBOOLE_1:7;

the carrier of R 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 A3, RELSET_1:7;

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