let R be RelStr ; :: thesis: for S being SubRelStr of R
for T being SubRelStr of S holds T is SubRelStr of R
let S be SubRelStr of R; :: thesis: for T being SubRelStr of S holds T is SubRelStr of R
let T be SubRelStr of S; :: thesis: T is SubRelStr of R
A1: ( the carrier of S c= the carrier of R & the InternalRel of S c= the InternalRel of R ) by YELLOW_0:def 13;
( the carrier of T c= the carrier of S & the InternalRel of T c= the InternalRel of S ) by YELLOW_0:def 13;
then ( the carrier of T c= the carrier of R & the InternalRel of T c= the InternalRel of R ) by A1, XBOOLE_1:1;
hence T is SubRelStr of R by YELLOW_0:def 13; :: thesis: verum