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
( the InternalRel of S c= the InternalRel of R & the InternalRel of T c= the InternalRel of S ) by YELLOW_0:def 13;
then A1: the InternalRel of T c= the InternalRel of R ;
( the carrier of S c= the carrier of R & the carrier of T c= the carrier of S ) by YELLOW_0:def 13;
then the carrier of T c= the carrier of R ;
hence T is SubRelStr of R by A1, YELLOW_0:def 13; :: thesis: verum