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

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