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