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:27;

reconsider I = the InternalRel of R1 /\ the InternalRel of R2 as Relation of ( the carrier of R1 /\ the carrier of R2) by A2, ZFMISC_1:100;

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:27;

reconsider I = the InternalRel of R1 /\ the InternalRel of R2 as Relation of ( the carrier of R1 /\ the carrier of R2) by A2, ZFMISC_1:100;

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