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 S
let x be set ; :: thesis: ( x in the carrier of R /\ the carrier of S implies x is Element of S )
assume A1: x in the carrier of R /\ the carrier of S ; :: thesis: x is Element of S
the carrier of R /\ the carrier of S c= the carrier of S by XBOOLE_1:17;
hence x is Element of S by A1; :: thesis: verum