let L be RelStr ; :: thesis: for S, T being full SubRelStr of L st the carrier of S c= the carrier of T holds
the InternalRel of S c= the InternalRel of T
let S1, S2 be full SubRelStr of L; :: thesis: ( the carrier of S1 c= the carrier of S2 implies the InternalRel of S1 c= the InternalRel of S2 )
( the InternalRel of S1 = the InternalRel of L |_2 the carrier of S1 & the InternalRel of S2 = the InternalRel of L |_2 the carrier of S2 ) by YELLOW_0:def 14;
hence ( the carrier of S1 c= the carrier of S2 implies the InternalRel of S1 c= the InternalRel of S2 ) by Th5; :: thesis: verum