let R be RelStr ; :: thesis: R is full SubRelStr of R
( the carrier of R c= the carrier of R & the InternalRel of R c= the InternalRel of R ) ;
then reconsider R' = R as SubRelStr of R by YELLOW_0:def 13;
the InternalRel of R' = the InternalRel of R |_2 the carrier of R' by XBOOLE_1:28;
hence R is full SubRelStr of R by YELLOW_0:def 14; :: thesis: verum