let L be RelStr ; :: thesis: for S being SubRelStr of L
for X being Subset of S holds X is Subset of L
let S be SubRelStr of L; :: thesis: for X being Subset of S holds X is Subset of L
let X be Subset of S; :: thesis: X is Subset of L
( X c= the carrier of S & the carrier of S c= the carrier of L ) by YELLOW_0:def 13;
hence X is Subset of L by XBOOLE_1:1; :: thesis: verum