for R, S being non empty RelStr
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 )