let R be RelStr ; :: thesis: for S being full SubRelStr of R
for T being full SubRelStr of S holds T is full SubRelStr of R
let S be full SubRelStr of R; :: thesis: for T being full SubRelStr of S holds T is full SubRelStr of R
let T be full SubRelStr of S; :: thesis: T is full SubRelStr of R
reconsider T1 = T as SubRelStr of R by YELLOW_6:7;
A1: the carrier of T c= the carrier of S by YELLOW_0:def 13;
the InternalRel of S = the InternalRel of R |_2 the carrier of S by YELLOW_0:def 14;
then the InternalRel of T = ( the InternalRel of R |_2 the carrier of S) |_2 the carrier of T by YELLOW_0:def 14
.= the InternalRel of R |_2 the carrier of T by A1, WELLORD1:22 ;
then T1 is full by YELLOW_0:def 14;
hence T is full SubRelStr of R ; :: thesis: verum