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_{1} being strict RelStr st

( the carrier of b_{1} = the carrier of R1 \/ the carrier of R2 & the InternalRel of b_{1} = the InternalRel of R1 \/ the InternalRel of R2 )
; :: thesis: verum

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

( the carrier of b