let L be RelStr ; :: thesis: for S1, S2 being full SubRelStr of L st the carrier of S1 = the carrier of S2 holds
RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #)
let S1, S2 be full SubRelStr of L; :: thesis: ( the carrier of S1 = the carrier of S2 implies RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) )
the InternalRel of S1 = the InternalRel of L |_2 the carrier of S1 by Def14;
hence ( the carrier of S1 = the carrier of S2 implies RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of S2, the InternalRel of S2 #) ) by Def14; :: thesis: verum