let R, S be non empty RelStr ; :: thesis: for x being Element of (R [*] S) holds
( x in the carrier of R or x in the carrier of S \ the carrier of R )
let x be Element of (R [*] S); :: thesis: ( x in the carrier of R or x in the carrier of S \ the carrier of R )
x in the carrier of (R [*] S) ;
then x in the carrier of S \/ the carrier of R by Def2;
then x in the carrier of R \/ ( the carrier of S \ the carrier of R) by XBOOLE_1:39;
hence ( x in the carrier of R or x in the carrier of S \ the carrier of R ) by XBOOLE_0:def 3; :: thesis: verum