let R, S be non empty RelStr ; :: thesis: for x being set st x in the carrier of R /\ the carrier of S holds
x is Element of R
let x be set ; :: thesis: ( x in the carrier of R /\ the carrier of S implies x is Element of R )
assume A1: x in the carrier of R /\ the carrier of S ; :: thesis: x is Element of R
the carrier of R /\ the carrier of S c= the carrier of R by XBOOLE_1:17;
hence x is Element of R by A1; :: thesis: verum