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₁ 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