set X = the carrier of R1 \/ the carrier of R2;
set I = the InternalRel of R1 \/ the InternalRel of R2;
A2: the InternalRel of R1 \/ the InternalRel of R2 c= [: the carrier of R1, the carrier of R1:] \/ [: the carrier of R2, the carrier of R2:] by XBOOLE_1:13;
set X1 = the carrier of R1;
set X2 = the carrier of R2;
( the carrier of R1 c= the carrier of R1 \/ the carrier of R2 & the carrier of R2 c= the carrier of R1 \/ the carrier of R2 ) by XBOOLE_1:7;
then ( [: the carrier of R1, the carrier of R1:] c= [:( the carrier of R1 \/ the carrier of R2),( the carrier of R1 \/ the carrier of R2):] & [: the carrier of R2, the carrier of R2:] c= [:( the carrier of R1 \/ the carrier of R2),( the carrier of R1 \/ the carrier of R2):] ) by ZFMISC_1:96;
then [: the carrier of R1, the carrier of R1:] \/ [: the carrier of R2, the carrier of R2:] c= [:( the carrier of R1 \/ the carrier of R2),( the carrier of R1 \/ the carrier of R2):] by XBOOLE_1:8;
then reconsider I = the InternalRel of R1 \/ the InternalRel of R2 as Relation of ( the carrier of R1 \/ the carrier of R2) by A2, XBOOLE_1:1;
set RR = RelStr(# ( the carrier of R1 \/ the carrier of R2),I #);
( the carrier of RelStr(# ( the carrier of R1 \/ the carrier of R2),I #) = the carrier of R1 \/ the carrier of R2 & the InternalRel of RelStr(# ( the carrier of R1 \/ the carrier of R2),I #) = I ) ;
hence ex b₁ being strict RelStr st
( the carrier of b₁ = the carrier of R1 \/ the carrier of R2 & the InternalRel of b₁ = the InternalRel of R1 \/ the InternalRel of R2 ) ; :: thesis: verum