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 b1 being strict RelStr st
( the carrier of b1 = the carrier of R1 \/ the carrier of R2 & the InternalRel of b1 = the InternalRel of R1 \/ the InternalRel of R2 )
; verum